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