FindEquationalProof[
In[]:=
AxiomaticTheory[]
Out[]=
{AbelianGroupAxioms,AbelianHigmanNeumannAxioms,AbelianMcCuneAxioms,BooleanAxioms,GroupAxioms,HigmanNeumannAxioms,HillmanAxioms,HuntingtonAxioms,McCuneAxioms,MeredithAxioms,MonoidAxioms,RingAxioms,RobbinsAxioms,SemigroupAxioms,ShefferAxioms,WolframAlternateAxioms,WolframAxioms,WolframCommutativeAxioms}
In[]:=
AxiomaticTheory["RingAxioms"]
Out[]=
In[]:=
AxiomaticTheory["RingAxioms","NotableTheorems"]
Out[]=
ZeroIsAbsorbing
∀
a.
a.⊗

0


0
,MinusOneYieldsInverse
∀
a.

1
⊗a.
a.

In[]:=
FindEquationalProof
∀
a.
a.⊗

0


0
,"RingAxioms"
Out[]=
In[]:=
%["ProofGraph"]
Out[]=
In[]:=
AxiomaticTheory["WolframAxioms","NotableTheorems"]
Out[]=
In[]:=
FindEquationalProof[a.·b.b.·a.,"WolframAxioms"]["ProofGraph"]
Out[]=
​
In[]:=
po=FindEquationalProof[a.·b.b.·a.,"WolframAxioms"];
In[]:=
KeySelect[po["ProofDataset"],First[#]==="CriticalPairLemma"&][All,"Statement"]
Out[]=
In[]:=
Values[%][[1]]
Out[]=
In[]:=
Normal[%]
Out[]=
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
In[]:=
FindEquationalProof[a.·b.b.·a.,Append[AxiomaticTheory["WolframAxioms"],ForAll[{a.,b.,c.},a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))]]]["ProofGraph"]

Distance in proof space

Nearby results are ones that can be reached from each other by very short proofs

Space of equations

Motion is proof from one equations to another

Light cone [?]

Given a collection of math equations [or generally statements], we can make a map of mathematics; where the distance between statements is the proof distance.

Points in statement space

Mathematical intractability tensor

Power/generality of the axiom system ~ mass [?]

Time evolution here is the evolution of the field of mathematics

We start with certain axioms/statements .... but now we evolve to have certain other statements
Abstraction tower: is like a geodesic bundle
Gravity : presence of intractability

Mass ~ density of computational irreducibility

Event horizons in space of mathematics

Constructibility:

Non-constructible results are behind event horizons [no finite-time geodesic can reach them]

Imagine a cloud of finitely-provable statements

Weak cosmic censorship

Claim: if enough equivalences between proofs exist, then only finite proofs can ever exist

A bundle of proofs with certain equivalences between them : geodesic bundle

Making a physics of metamathematics

Godel sentence for physics

[We have a computer that is simulating the universe, implemented in the universe:
simply predict the outcome of that computation]

Assume we have the statement: this universe exists
​