metamath(1)

🌸 NAME 🌸

metamath — formal proof verifier and proof assistant 🫶

✨ SYNOPSIS ✨

metamath [ commands | file ]

💖 DESCRIPTION 💖

okay so metamath is a formal proof verifier and a proof assistant for the Metamath language. it's giving math girlboss, no cap 🧮✨

you can boot it up two ways: feed it a series of commands, or hand it a data base file — and once it's up, you can explore that thing interactively. literally so fun.

for the deets on the Metamath language and the command-line interface, just type help right into the command prompt 💅 or read the Metamath book [1], which should have been installed along with the package — so check ur local filesystem bestie, it's probably right there.

🦋 LANGUAGE 🦋

a Metamath database is literally just a sequence of three kinds of tokens, separated by white space (and "white space" here means any sequence of one or more white space characters, periodt).

the token categories:

• keyword tokens — the set is exactly: ${, $}, $c, $v, $f, $e, $d, $a, $p, $., $=, $(, $), $[, and $]
• label tokens — any combination of letters, digits, and the characters hyphen, underscore, and period. the label of an assertion is what you use to refer to it in a proof 👑
• math symbol tokens — any combination of the 93 printable ascii(7) characters other than $

⚠️ the latter four keywords — $(, $), $[, and $] — are called auxiliary or preprocessing keywords. iykyk.

🌈 all tokens are case-sensitive. do not play with that.

💜 the statements, one by one 💜

• $( comment $) — comments. they get ignored, they're just there for the aesthetic 🙈
• $[ file $] — include the contents of a file. like a lil import, slay.
• ${ statements $} — a scoped block of statements. a math symbol becomes active when it's declared and stays active until the end of the block it was declared in. main character energy: it's only on stage for its own scene ✨
• $v symbols $. — declare symbols as variables. a variable may not be declared a second time while it's active, but it may be declared again (as a variable, but not as a constant) after it becomes inactive.
• $c symbols $. — declare symbols as constants. a constant must be declared in the outermost block and may not be declared a second time. no reruns, babe 💀
• label $f constant variable $. — a variable-type hypothesis, aka specifying the nature or type of a variable (like let x be an integer.). a variable must have its type specified in a $f statement before it may be used in a $e, $a, or $p statement. and there may not be two active $f statements containing the same variable. sorry, no duplicates 🚫
• label $e constant symbols $. — a logical hypothesis, expressing a logical truth (like assume x is prime) that must be established in order for an assertion requiring it to also be true. it's giving conditional 🎀
• $d variables $. — disjoint variable restriction. for distinct active variables, it forbids the substitution of one variable with another. keep them separated bestie ✌️
• label $a constant symbols $. — axiomatic assertion. the OGs, the unproven foundations 👑
• label $p constant symbols $= proof $. — provable assertion. the proof is a sequence of statement labels. this label sequence serves as a set of instructions that the Metamath program uses to construct a series of math symbol sequences. the construction must ultimately result in the math symbol sequence contained between the $p and $= keywords of the $p statement. for details, see section 4.3 in [1] 📖

💡 proofs are most easily written using the interactive prompt in metamath. do it that way, fr fr.

🎀 FILES 🎀

• /usr/share/metamath — data base files for several formal theories. ur starter pack 🍓

💫 SEE ALSO 💫

• [1] Norman Megill: Metamath, A Computer Language for Pure Mathematics.

and that's the whole page bestie!! brought to you by Metamath, dated 2018-02-04, living in the User Manuals section as page metamath(1) — obsessed with her honestly 💖✨ bye!!