Consider the “current state of math” as a collection of symbolic expressions

Addition facts:
In[]:=
Table[eq[Nest[s,0,i+j],plus[Nest[s,0,i],Nest[s,0,j]]],{i,3},{j,3}]
Out[]=
{{eq[s[s[0]],plus[s[0],s[0]]],eq[s[s[s[0]]],plus[s[0],s[s[0]]]],eq[s[s[s[s[0]]]],plus[s[0],s[s[s[0]]]]]},{eq[s[s[s[0]]],plus[s[s[0]],s[0]]],eq[s[s[s[s[0]]]],plus[s[s[0]],s[s[0]]]],eq[s[s[s[s[s[0]]]]],plus[s[s[0]],s[s[s[0]]]]]},{eq[s[s[s[s[0]]]],plus[s[s[s[0]]],s[0]]],eq[s[s[s[s[s[0]]]]],plus[s[s[s[0]]],s[s[0]]]],eq[s[s[s[s[s[s[0]]]]]],plus[s[s[s[0]]],s[s[s[0]]]]]}}
In[]:=
ExpressionTree/@Flatten[%7]
Out[]=

,
,
,
,
,
,
,
,

Each relation here is like a hyperedge, with certain shared atoms
Hyperedges can be combined through a token-event mechanism

Other examples:
boolean equivalences, order relations (e.g. 7 > 5) etc.

Substitution requires the concept of replacing variables with whole expressions

Or some other metalogical assumption
e.g.
a==b&&b==ca==c
But also need a novelty generator (e.g. add tautologies)

Worth considering geodesics because math derivations are at least fairly direct

Multiway graph: multiple histories for math / multiple proof paths

State of math: ~space ; history of math: ~spacetime ; proof: ~timelike curve

Proof cones

Proxy for “distance between relations”: how far apart they appear in a textbook [cf Euclid]

Perceptual distance in Euclid

Max speed in metamathematical space?

How fast can one reach another area in math?

Rederivation knits together metamathematical space (?)

[ Conceptually: record every time a mathematician writes down any derivation ]

Metamathematical motion

?Functors :: preservation of structure ?

Rulial version: all possible “mathematical laws” / all possible metalogics

A particular rulial frame = particular metalogic

Theorem proving

Substitution lemma
Critical pair lemma

Definitions are just abstract atoms

If two relations refer to the same thing, they just connect to the same atom....

Is it only the atoms that are shared, or are common subexpressions also shared?

Instead of ordered hyperedges, use trees...

Generalization of ordered hypergraph; instead of simple chain, have tree. ? Analogy in causal multiway system
Transformations on expression trees instead of hyperedges ? [ Or have expression instead of hypergraph ]
unordered [ tree1, tree2, ... ]

Expression derivation

Out[]=

Rules of inference

Take two statements; make another
,
,
In[]:=
TreeExtract
,2
Out[]=
In[]:=
TreeExtract
,{2,2}
Out[]=

Axioms are statements in the initial state; evolution is rules of inference

Spacelike surfaces are all possible statements of math at a particular time
Light cone of a given initial set of statements are the results for a single axiom system

E.g. my Boolean axiom has a light cone that contains all statements of Boolean algebra

Causal dependence: which inferences affect which others : i.e. which inferences are in proof chains

Ruliad limit: all possible initial states + all possible rules of inference

Model: add more statements e.g. in the initial state  more things can be generated

E.g. more is true about a specific group than a general group

Add too much “energy” in models and you get to a normal form, i.e. a spacelike singularity [?]

Every shortest inference chain is a geodesic... (i.e. every “best derivation”)

The more axioms/statements one adds, the closer one gets to decidability (?)

Mathematical assertion ~ mass ; too much of it and you get a black hole (?)

E.g. a group: the more relations you add, the smaller the group gets... The smaller the group, the more identities between words are generated

Time dilation: you either drill down and make proofs about the original thing you’re talking about ... or you have to “move” to talk about something different ... then you use some of your laws of inference to make that move....

If you stay in one area of math, you can make more proofs than if you try to make proofs about different kinds of things....
Twin paradox for mathematicians: a mathematician who keeps on exploring new areas won’t be able to prove as much.... because they’re using their inference rate to move rather than to “prove down” (i.e. to make a longer proof about a specific thing)