You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
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]