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[]=
ZeroIsAbsorbinga.⊗,MinusOneYieldsInverse⊗a.
∀
a.
0
0
∀
a.
1
a.
In[]:=
FindEquationalProofa.⊗,"RingAxioms"
∀
a.
0
0
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
Distance in proof space
Nearby results are ones that can be reached from each other by very short proofs
Space of equations
Space of equations
Motion is proof from one equations to another
Light cone [?]
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.
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
Points in statement space
Mathematical intractability tensor
Mathematical intractability tensor
Power/generality of the axiom system ~ mass [?]
Time evolution here is the evolution of the field of mathematics
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
Mass ~ density of computational irreducibility
Event horizons in space of mathematics
Event horizons in space of mathematics
Constructibility:
Constructibility:
Non-constructible results are behind event horizons [no finite-time geodesic can reach them]
Imagine a cloud of finitely-provable statements
Imagine a cloud of finitely-provable statements
Weak cosmic censorship
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
A bundle of proofs with certain equivalences between them : geodesic bundle
Making a physics of metamathematics
Making a physics of metamathematics
Godel sentence for physics
Godel sentence for physics
[We have a computer that is simulating the universe, implemented in the universe:
simply predict the outcome of that computation]
[We have a computer that is simulating the universe, implemented in the universe:
simply predict the outcome of that computation]
simply predict the outcome of that computation]
Assume we have the statement: this universe exists