#### Where do human-found theorems live in metamathematical space?

Where do human-found theorems live in metamathematical space?

Cf where in 3D x,y,z space did people build cities on earth?

## Boolean Algebra

Boolean Algebra

#### Entailment cone should give the true theorems, but not as efficiently

Entailment cone should give the true theorems, but not as efficiently

#### Can we tighten up what we find in the “entailment target/retention zone” [ “directed entailments” ]

Can we tighten up what we find in the “entailment target/retention zone” [ “directed entailments” ]

Ordinary theorem proving: we know the target, we want to find a single path

Traditional entailment cone: the entailments go out in all directions ... as opposed to making a “phased array” or an antenna in a particular direction

### What are the proofs of interesting statements like?

What are the proofs of interesting statements like?

In[]:=

interesting=First/@{{a==a⋀a,"idempotent law for and"},{a==a⋁a,"idempotent law for or"},{a⋀b==b⋀a,"commutativity for and"},{a⋁b==b⋁a,"commutativity for or"},{a==a,"law of double negation"},{a⋀a==b⋀b,"definition of false (law of noncontradiction)"},{a⋁a==b⋁b,"definition of true (law of excluded middle)"},{(a⋁b)==a⋀b,"de Morgan law"},{(a⋀b)==a⋁b,"de Morgan law"},{a==a⋀(a⋁b),"absorption law"},{a==a⋁a⋀b,"absorption law"},{(a⋀b)⋀c==a⋀(b⋀c),"associativity of and"},{(a⋁b)⋁c==a⋁(b⋁c),"associativity of or"}};

In[]:=

AxiomaticTheory["BooleanAxioms"]

Out[]=

a.⊗b.b.⊗a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗a.,a.⊗b.⊕a.,a.⊕b.b.⊕a.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)

∀

{a.,b.}

∀

{a.,b.,c.}

∀

{a.,b.}

b.

∀

{a.,b.}

b.

∀

{a.,b.}

∀

{a.,b.,c.}

In[]:=

interesting/.{Square->OverBar,Vee->CirclePlus,Wedge->CircleTimes}

Out[]=

aa⊗a,aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a,⊗a⊗b,⊕a⊕b,⊗,⊕,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)

a

a

b

a

b

a⊕b

a

b

a⊗b

a

b

In[]:=

FindReplacePath[ForAll[a,aa⊗a],AxiomaticTheory["BooleanAxioms"]]

Out[]=

Statementa⊗aa,PathTestSuccess,RewriteTestSuccess,Justification{{{Axiom,1},Right,{}},{{Axiom,3},Right,{}},{{Axiom,2},Left,{}}},RewritesReplace[x1_x1⊕x2$11_⊗]/*ReplaceAll[x2$11_a._],Replace[x1_⊗x2_⊕x1_⊗x3_x1⊗(x2⊕x3)],Replace[x1_⊗(x2_⊕)x1],Path{a._⊗a._,a._⊗a._⊕a._⊗,a._⊗(a._⊕),a._}

x2$11_

x2_

a._

a._

In[]:=

FindEquationalProof[ForAll[a,aa⊗a],AxiomaticTheory["BooleanAxioms"]]

Out[]=

ProofObject

In[]:=

FindReplacePath[ForAll[{a,b,c},#],AxiomaticTheory["BooleanAxioms"],"Path"]&/@aa⊗a,aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a,⊗a⊗b,⊕a⊕b,⊗,⊕,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)

a

a

b

a

b

a⊕b

a

b

a⊗b

a

b

x2

b

x2

b

Out[]=

In[]:=

Length/@%

Out[]=

{4,4,2,2,16,6,6,704,704,34,36,205,205}

NOTE: LeafCount wrong because of _’s

In[]:=

MapThread[ListLinePlot[#,Frame->True,PlotLabel->#2]&,Map[LeafCount,%9,{2}],aa⊗a,aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a,⊗a⊗b,⊕a⊕b,⊗,⊕,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)]

a

a

b

a

b

a⊕b

a

b

a⊗b

a

b

Out[]=

,

,

,

,

,

,

,

,

,

,

,

,

#### Note that this is after cut elimination ....

Note that this is after cut elimination ....

#### Approximate the branching ratio for the entailment cone

Approximate the branching ratio for the entailment cone

#### With intermediate lemmas

With intermediate lemmas

Wannabe theorems:

I.e. there are no new variables generated.... [at least after canonicalization]

## Other Axiom Systems

Other Axiom Systems

#### [ There are 3 proofs here; ATP found 1 ] [ There are many theorems; you pick the one you want ]

[ There are 3 proofs here; ATP found 1 ] [ There are many theorems; you pick the one you want ]

#### ATP is good if you already know the theorem you want

ATP is good if you already know the theorem you want

#### Discovering new theorems (e.g. my Boolean algebra axiom) is hard with ATP

Discovering new theorems (e.g. my Boolean algebra axiom) is hard with ATP

### General approach: use models to find plausible theorems

General approach: use models to find plausible theorems

Start from the axioms and find all models consistent with the axioms ... then ask what relations satisfy those models

## Directed Theorem Enumeration

Directed Theorem Enumeration

#### Instead of making the whole entailment cone, we only want “interesting theorems”

Instead of making the whole entailment cone, we only want “interesting theorems”

### In the Metamath database, we’re seeing a skeleton of the entailment cone

In the Metamath database, we’re seeing a skeleton of the entailment cone

## Metamath Database

Metamath Database

#### Imagine the entailment cone from the axioms of set theory

Imagine the entailment cone from the axioms of set theory

#### The MM database has a very thin skeleton of that entailment cone

The MM database has a very thin skeleton of that entailment cone

#### For the sake of argument, let’s assume MM’s proofs are minimal

For the sake of argument, let’s assume MM’s proofs are minimal

#### Can we estimate whether the skeleton is uniform across the entailment cone

Can we estimate whether the skeleton is uniform across the entailment cone

Guess is it’s not uniform in the EC, but instead it’s built out in towers....

Is there something special about the towers?

#### The big point is that higher-level math is possible; therefore having a sparse collection of towers may be “enough”

The big point is that higher-level math is possible; therefore having a sparse collection of towers may be “enough”

I.e. you can talk about math without going through all the detail of the whole entailment cone

#### What are the TEGs of the MM database?

What are the TEGs of the MM database?

The substitution entailment is more complicated in MM [ but it’s a simpler form of substitution, where it just replaces the variables ]

#### Each definition introduces a function symbol....

Each definition introduces a function symbol....

### MM is embedding all math in an explicit entailment graph ...

MM is embedding all math in an explicit entailment graph ...

But most mathematical conclusions (AKA mathematical motion) never has to look down to axioms/emes/....

E.g. in physics we have laws of motion that don’t talk about the atoms of space....

Analog in math is “human-level proofs”

[ E.g. Euclid picked “human-like axioms” ]

Extreme coarse graining:

In a math result, you’re not necessarily talking about something very specific at the level of axioms, and certainly not at the level of emes....