Metamath

http://us.metamath.org/mpeuni/mmset.html#proofs
Statements
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

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

Substitution is 2 inputs, 1 output