I could choose to “contextualize” my math experiments by adding a bunch of data to each end of each string....

Theorems in math A turns into B: physics A evolves to B

Each “theorem path” is like a transition amplitude for QM

mw=UndirectedGraph[ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},"A",8,"StatesGraph"]]
Out[]=
In[]:=
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},"A",8,"BranchialGraph"]
Out[]=

What is the analog in math of coarse graining in physics?

Nearby theorems: corollaries....
Some theorems are shortly provable from others; start with a bundle of “nearby terms”
Powerful theorem: big backbone in the graph

In actually doing math, you don’t go on a long path; you use theorems you already have, and go on a fairly short path.

The refactoring of axioms : what is the relation to abstraction?

Speciation in math: event horizons in the MW graph might correspond to the breaking off of different fields of math...

Note: vertex list is different in this case:
In[]:=
mwr=SimpleGraph[UndirectedGraph[ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&[{"A""AB","BB""A"}],"A",8,"StatesGraph"]]]
Out[]=
If we are tracing all possible paths, which lemma is most worth introducing to shorten the average path?
In[]:=
Histogram[GraphDistance[mw,#[[1]],#[[2]]]&/@Tuples[VertexList[mw],2]]
Out[]=
In[]:=
Histogram[GraphDistance[mwr,#[[1]],#[[2]]]&/@Tuples[VertexList[mwr],2]]
Out[]=
In[]:=
Mean[GraphDistance[mwr,#[[1]],#[[2]]]&/@Tuples[VertexList[mwr],2]]//N
Out[]=
3.86028
Want to find most common subsequence in here:
In[]:=
FindShortestPath[mw,#[[1]],#[[2]]]&/@Tuples[VertexList[mw],2]
In[]:=
Function[newax,With[{mw=SimpleGraph[UndirectedGraph[ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&[Join[{"A""AB","BB""A"},newax]],"A",8,"StatesGraph"]]]},Mean[Flatten[GraphDistanceMatrix[mw]]]//N]][{}]
Out[]=
3.86028
[[[ could prune possible lemmas by a factor of 2 ]]]
[[ Also get too far out in metamathematical space .... ]]
In[]:=
ResourceFunction["ParallelMapMonitored"][Function[newax,With[{mw=SimpleGraph[UndirectedGraph[ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&[Append[{"A""AB","BB""A"},Rule@@newax]],"A",8,"StatesGraph"]]]},Mean[Flatten[GraphDistanceMatrix[mw]]]//N]],Tuples[VertexList[mwr],2]]
During evaluation of In[2]:=
LinkObject
:Unable to communicate with closed link LinkObject[59549@10.20.50.7,59550@10.20.50.7,644,82].
During evaluation of In[2]:=
KernelObject
:Subkernel connected through KernelObject
Name: threadripper
KernelID: 73
 appears dead.
During evaluation of In[2]:=
Parallel`Developer`QueueRun
::req
:Requeueing evaluations {21} assigned to KernelObject
Name: threadripper
State: defunct
.
During evaluation of In[2]:=
LaunchKernels
:Kernel KernelObject
Name: threadripper
State: defunct
 resurrected as KernelObject
Name: threadripper
KernelID: 94
.
During evaluation of In[2]:=
LinkObject
:Unable to communicate with closed link LinkObject[59575@10.20.50.7,59576@10.20.50.7,657,95].
During evaluation of In[2]:=
KernelObject
:Subkernel connected through KernelObject
Name: threadripper
KernelID: 86
 appears dead.
During evaluation of In[2]:=
Parallel`Developer`QueueRun
::req
:Requeueing evaluations {8} assigned to KernelObject
Name: threadripper
State: defunct
.
During evaluation of In[2]:=
LaunchKernels
:Kernel KernelObject
Name: threadripper
State: defunct
 resurrected as KernelObject
Name: threadripper
KernelID: 95
.
During evaluation of In[2]:=
LinkObject
:Unable to communicate with closed link LinkObject[59573@10.20.50.7,59574@10.20.50.7,656,94].
During evaluation of In[2]:=
General
:Further output of LinkObject::linkd will be suppressed during this calculation.
During evaluation of In[2]:=
KernelObject
:Subkernel connected through KernelObject
Name: threadripper
KernelID: 85
 appears dead.
During evaluation of In[2]:=
General
:Further output of KernelObject::rdead will be suppressed during this calculation.
During evaluation of In[2]:=
Parallel`Developer`QueueRun
::req
:Requeueing evaluations {9} assigned to KernelObject
Name: threadripper
State: defunct
.
During evaluation of In[2]:=
General
:Further output of Parallel`Developer`QueueRun::req will be suppressed during this calculation.
During evaluation of In[2]:=
LaunchKernels
:Kernel KernelObject
Name: threadripper
State: defunct
 resurrected as KernelObject
Name: threadripper
KernelID: 96
.

Introducing a lemma is like changing your foliation

Axiom Systems

3.6 Euclidean Plane Geometry

The axioms of Euclidean plane geometry are the axioms of predicate logic together with the thirteen axioms below. This formulation of the axioms is taken from Tarski's paper "What is elementary geometry?". As is mentioned in his paper, these axioms are complete (syntactically) and consistent. Tarski claims in his book A Decision Method for Elementary Algebra and Geometry that these axioms describe essentially the same geometry as Hilbert (who first formalized Euclid's axioms).
The sets  and  for Euclidean plane geometry are defined as follows.