## Metamath

Metamath

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

### Metamath data

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/twoplustwo.mm"]]

f3[ϕ_,ψ_,χ_]↔f2[f2[ϕ_,ψ_],χ_]

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

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....

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

{atom1,atom2,atom3,atom4}

#### Theorem dependency graph is the deduplicated TEG

Theorem dependency graph is the deduplicated TEG

#### Two forms of “knitting”:

1. Structure of the expression tree/hypergraph

2. Connection through evaluation

Two forms of “knitting”:

1. Structure of the expression tree/hypergraph

2. Connection through evaluation

1. Structure of the expression tree/hypergraph

2. Connection through evaluation

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

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

“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...

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

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 ]

[ 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...

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

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

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@;

In[]:=

Take[vertexNameAssociation,10]

Out[]=

1cau_seq.has_mul._proof_1,2preorder.to_has_lt,3differentiable_at.smul_const,4mul_action.to_has_scalar,5tendsto_multiset_sum,6multiset.sum,7neg_of_mul_pos_right,8linear_order.to_partial_order,9nat.bit_lt_bit_iff,10decidable_linear_ordered_semiring.to_linear_ordered_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?

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?

What is the LoI for ATP?

For individual steps in the proof:

{theorem1,theorem2}->{theorem3}

#### Example of “quantum math”: multiple proof paths:

Example of “quantum math”: multiple proof paths:

#### What is the homotopic structure of a particular axiom system?

What is the homotopic structure of a particular axiom system?

#### If proof-space is like Swiss cheese ...

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?

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]

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

## Possible Toy Examples

Possible Toy Examples

#### WPP models

WPP models

#### String substitution systems

String substitution systems

We have a collection of strings that represents a state

[Atoms are characters and positions]

#### Arbitrary axiom systems

Arbitrary axiom systems

#### Boolean algebra ?

Boolean algebra ?

#### Plus identities

Plus identities

#### LEAN/Metamath

LEAN/Metamath