In[]:=

CloudGet["https://wolfr.am/PJKo9Lnq"];EuclidGraphLarge[Subgraph[euc,VertexOutComponent[euc,<|"Book"->1,"Theorem"->5|>,2]]]

Out[]=

#### This is a “proof path”

This is a “proof path”

In[]:=

ReverseGraph[%]

Out[]=

In[]:=

CloudGet["https://wolfr.am/PJKo9Lnq"];EuclidGraphSmall[Subgraph[euc,VertexOutComponent[euc,<|"Book"->12,"Theorem"->3|>]],"Intense"]

Out[]=

In[]:=

ReverseGraph[%]

Out[]=

#### Generational steps ~ transitive closure

Generational steps ~ transitive closure

In[]:=

CloudGet["https://wolfr.am/PJKo9Lnq"];ReverseGraph[EuclidGraphSmall[TransitiveReductionGraph[Subgraph[euc,VertexOutComponent[euc,<|"Book"->12,"Theorem"->18|>]]],"Intense"]]

Out[]=

In[]:=

CloudGet["https://wolfr.am/PJKo9Lnq"];Row[Riffle[ReverseGraph/@(EuclidGraphLarge[#[Subgraph[euc,VertexOutComponent[euc,<|"Book"->12,"Theorem"->18|>,1]]],ImageSize->{Automatic,180}]&/@{Identity,TransitiveReductionGraph}),Spacer[50]]]

Out[]=

#### This is a many-theorems-in, one-theorem-out token-event graph

This is a many-theorems-in, one-theorem-out token-event graph

Where is the proof path within the Euclid-populated entailment cone

#### Populated entailment cone

Populated entailment cone

Skeleton entailment cone

[~ Lewis & Clark only surveyed some portions of the land ]

The manner of population reflects the operation of mathematical observers....

#### Superaxioms are the “supernamed axioms” from the populated entailment cone

[From the raw entailment cone; (AKA barren entailment cone; greenfield entailment cone; uninhabited; unobserved) ]

popular populated

Superaxioms are the “supernamed axioms” from the populated entailment cone

[From the raw entailment cone; (AKA barren entailment cone; greenfield entailment cone; uninhabited; unobserved) ]

popular populated

[From the raw entailment cone; (AKA barren entailment cone; greenfield entailment cone; uninhabited; unobserved) ]

popular populated

[ Like Chicago, where railroads meet ]

## Geometry

Geometry

Euclid’s version:

#### Effectively entailment fabric from a union of proof graphs:

Effectively entailment fabric from a union of proof graphs:

Not the full fabric; just a single ATP thread for each theorem

## Pythagorean theorem

Pythagorean theorem

#### Summarized version of branchial graph:

Summarized version of branchial graph:

## Pythagorean MetaMath

Pythagorean MetaMath

This is the source for proofs of theorems....

#### Most “complex” theorem:

Most “complex” theorem:

#### What is the distribution of populated proof path sizes for different areas?

What is the distribution of populated proof path sizes for different areas?

## Top 100 Theorems

Top 100 Theorems

Modifying pythi ....

[Color code by area]