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

Metamath data

All we should need are: “atoms”/operators [ or symbols + argument structure], variables [slots], statements
f
f[x,y,z]
In[]:=
ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/geohot/twitchcoq/master/metamath/twoplustwo.mm"]]
http://us.metamath.org/mpeuni/df-3an.html
f3[ϕ_,ψ_,χ_]↔f2[f2[ϕ_,ψ_],χ_]

There are multiple filters in getting to a “valid” mathematical statement

1. Is it syntactically constructed correctly?
2. Does it follow from whatever axioms we’ve chosen?
x,y,z,f[x,y,z]

In WPP, there are no “syntax errors” in space....

{atom1,atom2,atom3,atom4}

Theorem dependency graph is the deduplicated TEG

Two forms of “knitting”:
1. Structure of the expression tree/hypergraph
2. Connection through evaluation

A given axiom system is effectively operating in a particular rulial reference frame

We can model this by starting with a certain set of axioms and then applying LoIs ... but this will be multicomputational ... so then we have to say “what choice of ref frame, i.e. what sequence of math-states” are we going to get?

“math-state”: particular set of asserted statements that represent the posited state of mathematics

An actual mathematician (human) sees only the coarse-grained version of the math-state...

ATP is like molecular dynamics; typical work by mathematicians is like fluid dynamics

[ At the fluid dynamics level, you need a “human-compatible language”]
[ as opposed to actual computer machine code, which is the molecular dynamics ]

Hilbert etc. believed that by going to the machine code level they were reaching bedrock...

And that by reaching bedrock they’d “solved math”

Mathematician is like a sculptor turning raw stone into something humans care about

I.e take the block of all math, and form a subpart of it that humans care about

Metamath/LEAN example

Given all MetaMath statements derived from given axioms .... what math-state do they make?
In those statements, there will be all sorts of symbols that appear
The math-state is a collection of statements (where each statement has a name)
In[]:=
vertexNameAssociation=Uncompress@
vertex association
;
In[]:=
Take[vertexNameAssociation,10]
Out[]=
1cau_seq.has_mul._proof_1,2preorder.to_has_lt,3differentiable_at.smul_const,4mul_action.to_has_scalar,5tendsto_multiset_sum,6multiset.sum,7neg_of_mul_pos_right,8linear_order.to_partial_order,9nat.bit_lt_bit_iff,10decidable_linear_ordered_semiring.to_linear_ordered_semiring
This is the number of hyperedges in the math-state:
In[]:=
Length[vertexNameAssociation]
Out[]=
107229

Different question: what is the “coarse-grained math state” of theorems we name in ordinary math?

How many distinct atoms are there in the math-state? I think it’s just the number of definitions

What is the LoI for ATP?

For individual steps in the proof:
{theorem1,theorem2}->{theorem3}

Example of “quantum math”: multiple proof paths:

What is the homotopic structure of a particular axiom system?

If proof-space is like Swiss cheese ...

[ Relation to computational irreducibility ]
Can one characterize areas of math in terms of the obstruction density in proof space?

Is a definition just a statement that includes some new symbol?

There’s enough in the Peano axioms that that operator that appears can reasonably be called Plus

There is a syntactic hypergraph of all the axioms... [maybe]

Possible Toy Examples

WPP models

String substitution systems

We have a collection of strings that represents a state
[Atoms are characters and positions]

Arbitrary axiom systems

Boolean algebra ?

Plus identities

LEAN/Metamath