## Metamath

Metamath

http://us.metamath.org/mpeuni/mmset.html#proofs

Statements

Definitions : gives a name to a statement

Functions / Constants / Variables

Definitions : gives a name to a statement

Functions / Constants / Variables

A well-formed statement is associated with the wff constant

⊢ is also a constant

#### Workflow: define possible symbolic expressions

Then see how some expressions can be derived from others by repeated substitution

Workflow: define possible symbolic expressions

Then see how some expressions can be derived from others by repeated substitution

Then see how some expressions can be derived from others by repeated substitution

Start with a giant ocean of syntactic expressions .... then see what chains of substitution there are within these....

Then there is some connected component that contains axioms we like

Then there is some connected component that contains axioms we like

#### Substitution is 2 inputs, 1 output

Substitution is 2 inputs, 1 output