## Flow of Efforts...

Flow of Efforts...

#### Basic goal: to find a minimal idealization of mathematics + metamathematics that allows us to study it in bulk...

Basic goal: to find a minimal idealization of mathematics + metamathematics that allows us to study it in bulk...

Mathematica + WL provides a good foundational framework

The various efforts of mathematical logic + ATP + proof assistants ... provide other, related frameworks

#### What is the essence of mathematics?

What is the essence of mathematics?

Assertion of statements as “true” [or at least entailed]

To be compared with physics where when some state is generated, one says that it happens

[ The mathematical observer can only observe something if that thing is present in metamathematical space ]

In the Tarski approach “X” vs X is what the observer “absorbs” vs. what’s actually out there

In the Tarski approach “X” vs X is what the observer “absorbs” vs. what’s actually out there

#### [Question of “X” vs “X is true”]

[Question of “X” vs “X is true”]

### Fundamental Characterization of Mathematics

Fundamental Characterization of Mathematics

#### Machine-level

Machine-level

[example is some human-level given in proof-assistant form]

#### Human-level [i.e. observer level]

Human-level [i.e. observer level]

#### Claim: to do human-level math you mostly just need human-level math

But ... to do computational paradigm stuff you need the machine level

Claim: to do human-level math you mostly just need human-level math

But ... to do computational paradigm stuff you need the machine level

But ... to do computational paradigm stuff you need the machine level

### The Process of Idealization

The Process of Idealization

Empirical version of what human-level math is:

Typical math papers

Math in Mathematica

Euclid

Typical math papers

Math in Mathematica

Euclid

Empirical version of “machine-level” math is:

ATP

Metamath

Proof assistant libraries

ATP

Metamath

Proof assistant libraries

### The Objects of Mathematics

The Objects of Mathematics

#### Basic math representation: symbolic expressions

Basic math representation: symbolic expressions

(which implicitly have pattern variables)

Out[]=

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

∀

{a.,b.,c.}

∀

a.

1

∀

a.

a.

1

Out[]=

ImpliesMcCuneAxiomsa.⊗d.,InverseOfComposite⊗,InverseOfInversea.,LeftIdentity⊗a.a.,LeftInverse⊗a.

∀

{a.,b.,c.,d.}

b.⊗(c.⊗)⊗⊗a.

c.

d.⊗b.

∀

{a.,b.}

a.⊗b.

b.

a.

∀

a.

a.

∀

a.

1

∀

a.

a.

1

#### Expression may be of the form lhs rhs or they may have other predicates

Expression may be of the form lhs rhs or they may have other predicates

but in the typical way pure math is represented, the expressions are supposed to have truth values.

#### This is a special case of computation: the number 3 isn’t a mathematical proposition

This is a special case of computation: the number 3 isn’t a mathematical proposition

#### First slicing of the “mathematical observer”: consider only expression that have a truth value

First slicing of the “mathematical observer”: consider only expression that have a truth value

I.e. the “raw material” of math is theorems [not e.g. algorithms]

### How Can We Idealize the Objects of Mathematics

How Can We Idealize the Objects of Mathematics

First level: symbolic expressions with heads, arguments, etc. and pattern variables

[ There are fixed, literal “constants” and/or “named functions” ]

Second level: there is nothing intrinsic about the named objects; just use function application for everything .... this is combinators

[ probably with every variable being a pattern variable ] [i.e. no S, K etc.]

[ There are fixed, literal “constants” and/or “named functions” ]

Second level: there is nothing intrinsic about the named objects; just use function application for everything .... this is combinators

[ probably with every variable being a pattern variable ] [i.e. no S, K etc.]

How does this compare to hypergraphs? In the math case, we’re imagine that we’re doing transformations on subtrees [i.e. that we have hierarchical structure]

We could represent everything in Polish notation, and have rules that appropriately walk around to emulate subtrees ... but to connect with math it’s easier to use tree structures if we want to connect with standard math notation etc.

Subtrees probably imitate the subtrees of human language (and/or the object/subobject organization that we put on the world)

#### Exercise: compile S, K combinators to tree substitutions with no variables [S on its own this should be fairly easy]

Exercise: compile S, K combinators to tree substitutions with no variables [S on its own this should be fairly easy]

#### Claim: Naming is an affordance by the observer ; a name is just a compression of a subtree with some structure

Claim: Naming is an affordance by the observer ; a name is just a compression of a subtree with some structure

The persistence of a name requires that certain subtrees persist. [E.g. the naming of a hurricane ... it’s realistic to name because it’s persistent ]

If things are “ground up” by entailment, there’s no point in naming them...

#### Potentially important feature: code = data (AKA you can operate on rules that are themselves used to operate on things)

Potentially important feature: code = data (AKA you can operate on rules that are themselves used to operate on things)

In physics, we do not imagine that there are “genuine lemmas” that let you jump ahead in the evolution of the universe; these are only in the mind of the observer

#### Claim: in the end most of the phenomena will be visible in NKS-style “string math”

Claim: in the end most of the phenomena will be visible in NKS-style “string math”

However, how the higher-level human observer interacts with that is not obvious

I.e. what equivalence classes of strings does the mathematical observer set up ?

### The Dynamics of Mathematics

The Dynamics of Mathematics

#### Primary action: proof (AKA entailment)

Primary action: proof (AKA entailment)

#### Typical pattern: given a few “objects”, an infinite collection are entailed

Typical pattern: given a few “objects”, an infinite collection are entailed

#### There is a machine-level version of entailment etc. ; there is also a human-level

There is a machine-level version of entailment etc. ; there is also a human-level

#### Machine-level entailment is just (“meaningless”) operations on symbolic expressions

Machine-level entailment is just (“meaningless”) operations on symbolic expressions

#### In a first approximation, mathematical observers only care about the objects of mathematics (i.e. mathematical statements)

In a first approximation, mathematical observers only care about the objects of mathematics (i.e. mathematical statements)

#### Each step in a proof takes statements in, and produces entailed statements out....

Each step in a proof takes statements in, and produces entailed statements out....

### Non-Cumulative Axiom Based Dynamics

Non-Cumulative Axiom Based Dynamics

#### [ “rulocumulative” dynamics ]

[ “rulocumulative” dynamics ]

The only transformation rules are defined by fixed axioms

Cumulative: additional transformations (i.e. code) are made from data, and can then be applied

Physics is intrinsically non-cumulative, except by virtue of mediation by the observer [who can choose to make certain correspondences]

### What Is the Basic Entailment?

What Is the Basic Entailment?

I.e. the laws of inference [which are the metalogic of the system]

The most basic is pure substitution

statement/.lhs<->rhs

This is probably all you can do for a general statement that is an arbitrary symbolic expression [this is what WL does, except for the “thermodynamic driving” of vs ]

[This is the elementary entailment; notice that it’s the same basic structure as in WPP]

#### Entailment for rule-like constructs (or logic-like constructs)

Entailment for rule-like constructs (or logic-like constructs)

a<->b/.lhs<->rhs

Then you can have “mix it up” entailments

### Comparison with WPP

Comparison with WPP

statement/.lhs<->rhs

This is a subtree substitution setup

{edge1,edge2,...}/.{edgepatt1,edgepatt2,...}->{newedge1,...}

Compare this with string substitution, CAs, TMs, etc.

### The Metamathematical Multiway Graph (AKA Entailment Graph)

The Metamathematical Multiway Graph (AKA Entailment Graph)

In[]:=

NestGraph[Values[substitutionLemmas[#,x_x_[x_]]]&,{x_x_[x_]},3]

Out[]=

In[]:=

NestGraph[Values[substitutionLemmas[#,x_x_[x_]]]&,{x_x_[x_]},3,GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2]

Out[]=

In[]:=

VertexList[%161]

Out[]=

{x_x_[x_],x_x_,x_x_[x_[x_]],x_x_[x_][x_[x_]],x_[x_]x_[x_],x_[x_]x_,x_x_[x_[x_[x_]]],x_x_[x_[x_][x_[x_]]],x_x_[x_[x_]][x_[x_[x_]]],x_[x_]x_[x_[x_]],x_x_[x_][x_],x_x_[x_][x_[x_[x_]]],x_x_[x_][x_[x_][x_[x_]]],x_x_[x_][x_[x_]][x_[x_][x_[x_]]],x_[x_]x_[x_][x_[x_]],x_[x_[x_]]x_[x_],x_[x_][x_[x_]]x_[x_],x_x_[x_[x_[x_[x_]]]],x_x_[x_[x_[x_][x_[x_]]]],x_x_[x_[x_[x_]][x_[x_[x_]]]],x_x_[x_[x_[x_]]][x_[x_[x_[x_]]]],x_[x_]x_[x_[x_[x_]]],x_x_[x_[x_][x_]],x_x_[x_[x_][x_[x_[x_]]]],x_x_[x_[x_][x_[x_][x_[x_]]]],x_x_[x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_x_[x_[x_][x_[x_]]][x_[x_[x_][x_[x_]]]],x_[x_]x_[x_[x_][x_[x_]]],x_x_[x_][x_][x_[x_][x_]],x_[x_]x_[x_][x_],x_x_[x_][x_[x_[x_[x_]]]],x_x_[x_][x_[x_[x_][x_[x_]]]],x_x_[x_][x_[x_[x_]][x_[x_[x_]]]],x_x_[x_][x_[x_[x_]]][x_[x_][x_[x_[x_]]]],x_[x_]x_[x_][x_[x_[x_]]],x_x_[x_][x_[x_][x_]],x_x_[x_][x_[x_][x_[x_[x_]]]],x_x_[x_][x_[x_][x_[x_][x_[x_]]]],x_x_[x_][x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_x_[x_][x_[x_][x_[x_]]][x_[x_][x_[x_][x_[x_]]]],x_[x_]x_[x_][x_[x_][x_[x_]]],x_x_[x_[x_]][x_[x_]],x_x_[x_[x_]][x_[x_[x_[x_]]]],x_x_[x_[x_]][x_[x_[x_][x_[x_]]]],x_x_[x_[x_]][x_[x_[x_]][x_[x_[x_]]]],x_x_[x_[x_]][x_[x_[x_]]][x_[x_[x_]][x_[x_[x_]]]],x_[x_]x_[x_[x_]][x_[x_[x_]]],x_x_[x_][x_[x_]][x_[x_]],x_x_[x_][x_[x_]][x_[x_][x_]],x_x_[x_][x_[x_]][x_[x_][x_[x_[x_]]]],x_x_[x_][x_[x_]][x_[x_][x_[x_][x_[x_]]]],x_x_[x_][x_[x_]][x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_x_[x_][x_[x_]][x_[x_][x_[x_]]][x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_[x_]x_[x_][x_[x_]][x_[x_][x_[x_]]],x_[x_[x_]]x_,x_[x_][x_[x_]]x_,x_[x_[x_]]x_[x_[x_]],x_[x_][x_[x_]]x_[x_[x_]],x_[x_[x_]]x_[x_][x_[x_]],x_[x_][x_[x_]]x_[x_][x_[x_]],x_[x_[x_[x_]]]x_[x_],x_[x_[x_][x_[x_]]]x_[x_],x_[x_[x_]][x_[x_[x_]]]x_[x_],x_[x_][x_]x_[x_],x_[x_][x_[x_[x_]]]x_[x_],x_[x_][x_[x_][x_[x_]]]x_[x_],x_[x_][x_[x_]][x_[x_][x_[x_]]]x_[x_]}

[bug:]

Given this mathematical setup, these are entailed statements...

Can we identify “named subtrees” that help us understand what’s going on?

Eventually, all “true” / entailed statements (presumably) show up ... though there’s no guarantee how many steps it will take....

#### How quickly are the true statements generated?

How quickly are the true statements generated?

Number trees based on this sequence:

[[ Probably a better approach is to treat each tree in terms of a binary digit sequence ]]

#### Is the proof graph confluent? [I.e. if you wait long enough you’ll always prove your favorite theorem, whatever path you take]

Is the proof graph confluent? [I.e. if you wait long enough you’ll always prove your favorite theorem, whatever path you take]

Alternative is that it might have event horizons.... Or it might just be too tree-like ....

### Can X be Proved?

Can X be Proved?

#### Straightforward approach: just find X in the full multiway proof graph

Straightforward approach: just find X in the full multiway proof graph

The proof from the original axioms is then the path (or tree) that gets you to the required X

[ It can be a tree if one starts from more than one axiom ]

#### Alternative: given a set of asserted theorems (AKA axioms) can one reach X in the forward entailment cone of those theorems?

Alternative: given a set of asserted theorems (AKA axioms) can one reach X in the forward entailment cone of those theorems?

It could in principle be reachable, but only by an arbitrarily long path ... hence undecidability

#### This approach to proof/truth is: if it’s produced, it’s “true”

This approach to proof/truth is: if it’s produced, it’s “true”

This is essentially constructive mathematics .... The notion that there is a “false” version of a statement that can be derived from the true version doesn’t really enter here

(In usual logic, it’s straightforward to negate a statement; here it is not. Given a “true” statement, there is no guarantee of exhibiting a corresponding false statement)

(In usual logic, it’s straightforward to negate a statement; here it is not. Given a “true” statement, there is no guarantee of exhibiting a corresponding false statement)

### ATP

ATP

Makes direct use of the concept of a “True”

Assume that something “self evident” is True, e.g. x == x

(If our only operators are composition and equality, the way we represent “True” is with x==x )

Our goal in ATP is to take axioms+hypothesis and derive True

This would imply that hypothesis is equivalent to True

This would imply that hypothesis is equivalent to True

(In a non-cumulative setup, you would just have a path graph that keeps on applying different axioms at each step...)

It’s a more complicated tree if it’s rulocumulative

It’s a more complicated tree if it’s rulocumulative

#### Can we flatten the graph from FindEquationalProof to a non-rulocumulative form?

Can we flatten the graph from FindEquationalProof to a non-rulocumulative form?

### Partial rulocumulativity

Partial rulocumulativity

One possibility: every time you’ve derived a new result, always use it

Other possibility: just pick a few results, and use them

Other possibility: just pick a few results, and use them

## Causal Graphs

Causal Graphs

#### These help track the fate of named objects ... because they show us how fragments of states get passed through

These help track the fate of named objects ... because they show us how fragments of states get passed through

#### The evolution graph ignores what’s “merely a spectator” and treats everything as being “involved”

The evolution graph ignores what’s “merely a spectator” and treats everything as being “involved”

## Potential Difference Between Math and Physics

Potential Difference Between Math and Physics

#### In math, we are always looking at large swaths of branchial space

In math, we are always looking at large swaths of branchial space

#### As math evolves, we as observers are more spread out in branchial space; our near-term future entailment cone is bigger

As math evolves, we as observers are more spread out in branchial space; our near-term future entailment cone is bigger

#### Motion in metamathematical/branchial space: exploring more math [charting the unknown in math]

Motion in metamathematical/branchial space: exploring more math [charting the unknown in math]

#### Time computational activity; in mathematics entailment is always “there to happen” ... but we may or may not choose to “make it happen” as observers. In physics, evolution is there to happen, but we may or may not choose foliations where it does

Time computational activity; in mathematics entailment is always “there to happen” ... but we may or may not choose to “make it happen” as observers. In physics, evolution is there to happen, but we may or may not choose foliations where it does

In both cases, it is the perception of the observer that “causes” time to be perceived as passing

#### Different proof paths can involve quite different areas of mathematics, or similar ones

Different proof paths can involve quite different areas of mathematics, or similar ones

I.e. to get to a certain statement, it could just be a bundle of nearby paths, or there could be homotopically distinct bundles

Is the proof continuously deformable at all stages, or is there an obstruction?

#### “Pure motion” in branchial space is about transporting a cluster of results in one area of math to another [i.e. the functor story]

“Pure motion” in branchial space is about transporting a cluster of results in one area of math to another [i.e. the functor story]

## Model Theory

Model Theory

Let’s imagine that we can define a “numeraire” for every statement

Given a model, both might turn into numbers ... and then there might be a result that every deduction must be a larger number

In x x[x] our “numeraire” is just the size of the tree. Now we have a result that says we can only get bigger trees...

This type of model is like a foliation....

#### Models break all possible expressions into equivalence classes, thereby defining which ones can be equal

Models break all possible expressions into equivalence classes, thereby defining which ones can be equal

(They can overdo it, like hash codes)

### What is the relation between a model and what an observer observes with coarse graining?

What is the relation between a model and what an observer observes with coarse graining?

For the integers, the model of Peano arithmetic that is the ordinary integers is effectively a coarse graining of the full symbolic representation of Peano arithmetic [?]

For group theory, we have abstract results about groups ;; but we can take a specific groups as our model, and doing that does lots of coarse graining and makes many equivalences that wouldn’t otherwise be there, be there....

#### How do we go from pure group theory, to the theory of a specific group?

How do we go from pure group theory, to the theory of a specific group?

The proof graph of

will give all the true statements of abstract group theory, with no additional relations (i.e statements that are true in particular for the free group)

When we add in the relations for a particular group [i.e. we add them as axioms], we will get more true statements ... and we get more relations (which are true statements)

To have a valid group, the defining relations must be consistent with the general properties of a group .... i.e. they produce extra connections in the proof graph

BUT they can never generate a node that was not present before... [except if the system is cumulative, then those extra edges can be turned into nodes]

BUT they can never generate a node that was not present before... [except if the system is cumulative, then those extra edges can be turned into nodes]

#### Normally making it a specific group adds edges which effectively put existing nodes together

Normally making it a specific group adds edges which effectively put existing nodes together

### [Lawvere’s model theory]

[Lawvere’s model theory]

## Relation to Formalized Math

Relation to Formalized Math

[ Analogy: We have empirical data about gravity between the Earth and the Moon ..... how can we use this to know about what happens with the atoms of space? ]

#### A piece of branchial space [for Euclid]

A piece of branchial space [for Euclid]

#### Proof graph for Euclid

Proof graph for Euclid

What are the entailments here?

Volume of past entailment cone for each theorem:

#### [Transitive reduction of proof graph is the always-leading-edge way of exploring math]

[Transitive reduction of proof graph is the always-leading-edge way of exploring math]

#### Euclid all theorems:

Euclid all theorems:

#### Emergent axioms of Boolean algebra:

Emergent axioms of Boolean algebra:

### If you add a new statement to the proof graph, it’ll have an entailment cone, and the overall graph will be bushier

If you add a new statement to the proof graph, it’ll have an entailment cone, and the overall graph will be bushier

### There are presumably many statements that we would call the Pythagorean theorem, but they are different in metamath...

There are presumably many statements that we would call the Pythagorean theorem, but they are different in metamath...

Depending on curvature in proof space ... there may be some separation or not of the geodesics

## Which Features Are Essential for a Human Mathematical Observer?

Which Features Are Essential for a Human Mathematical Observer?

#### Tree-iness

Tree-iness

#### Cumulative-ness / code = data

Cumulative-ness / code = data

### Or ... is a string multiway system a good model?

Or ... is a string multiway system a good model?

### If we want to preserve the “humanizability of mathematics”, we probably have to assume certain axioms

If we want to preserve the “humanizability of mathematics”, we probably have to assume certain axioms

Right now, it may be fine to assume CH is true or is false ... but the “wrong” assumption will lead to non-humanizable math [e.g. math that shreds to the molecular level ... so that it’s full of undecidability] [CH is like an investment, and we’re long in CH now....]

### How many elements are there in human-interesting metamathematical proof graphs?

How many elements are there in human-interesting metamathematical proof graphs?

How does it compare to the elements in the universe? [Given that in math we have a systematic way to use reducibility]

## Relativity for Metamathematics

Relativity for Metamathematics

#### It doesn’t matter in what order you prove the theorems, you can always get to the same math in the end

It doesn’t matter in what order you prove the theorems, you can always get to the same math in the end

There are many foliations of proof space; they are all ultimately equivalent

#### [ We need to find a case where time stops ... no further entailments ]

[ We need to find a case where time stops ... no further entailments ]

The fact that there are always more theorems to prove (at least at the machine level) speaks to the endless frontier of math

Could it be that there are no more human-level theorems to prove? No: because in metamathematics there is inevitable GR

For fundamental multicomputational reasons, the structure of proof space can’t just shred [~ 2nd Law etc. have to keep on holding]

#### Future of math could be ruliology .. except that it has a different aesthetic ... which is a human-derived aesthetic, which doesn’t match the machine-level approach

Future of math could be ruliology .. except that it has a different aesthetic ... which is a human-derived aesthetic, which doesn’t match the machine-level approach

~ machine learning takes over science ... with models we can never understand

## Structure of Bulk Metamathematics

Structure of Bulk Metamathematics

BA axiom is out in the wilderness of proof space ... without any continuum connection

#### Human mathematical observer ... extended in branchial space

Human mathematical observer ... extended in branchial space

Therefore conflates theorems that are trivially lemma-related to each other....

I.e. you have a theorem, and then you a halo of trivially related other theorems

### Main multicomputational fact: a mathematical observer extended in branchial space can be persistent, and not be shredded

Main multicomputational fact: a mathematical observer extended in branchial space can be persistent, and not be shredded

This is why human-level mathematics is possible.....

[But human-level ruliology may not be possible]

This why you don’t fall into ATPs immediately ... and people have been able to do math...

## Representation of Higher-Level Math

Representation of Higher-Level Math

We don’t go all the way to the formal bedrock ... because if we did it become incomprehensible

Going all the way to the bedrock is like shredding things. It’s not self-evident that you can jump between high-level representations .... you might have to go to the bedrock to say what’s happening

Rather than making a broad brush stroke statement .... it might shatter into pixie dust

[Does it shatter like the Cantor set...]

Can one preserve the continuum or not?

What is the metamathematical analog: i.e. as you iterate in proof space, the difference between nearby axioms/assumptions/... doesn’t have a big effect ..... vs. it gets shredded.

It doesn’t get shredded if you have the right kind of “observer equivalence class” ; we as physical observers have that, and we can grandfather that into mathematics....

[ But if we pick a weird observer equivalence class, it might get shredded ]

## Proof Graph vs. All Syntactically Possible Statements

Proof Graph vs. All Syntactically Possible Statements

#### The proof graph lives in a ocean of syntactically possible statements; many of them it never reaches

The proof graph lives in a ocean of syntactically possible statements; many of them it never reaches

If there is a definition of negation, we could check it never reaches both a statement and its negation

## Continuum for Observers and for Math

Continuum for Observers and for Math

#### A persistent observer necessarily believes in the continuum

A persistent observer necessarily believes in the continuum

### What is the relationship between this and the continuum inside mathematics?

What is the relationship between this and the continuum inside mathematics?

When the observer makes a model of mathematics, do they introduce the continuum?

#### Humans assume some degree of continuity

Humans assume some degree of continuity

The nontrivial fact is that that is consistent with the proof / entailment evolution ... and that what was a little region of continuity doesn’t get shredded

I.e. that the concept of a point, for example, is persistent

## Invention vs. Discovery for Math

Invention vs. Discovery for Math

It’s discovery in the sense that the ruliad is all out there....

It’s “invention” in the sense that it’s our fate what to observe, based on the history of our biology, culture, etc.

[In the sense that it depends on our mathematical technology, it’s invented]

Cumulative buildup: like self-invention of math

Discovered in the same sense that we discover aspects of the physical universe (“find the source of the Nile”)

There are only certain aspects of the physical universe that we sense ;; we are responsible (at some level) for what we can sense

We invent tech for observing the universe: microscope, telescope, amplifier, ...

We invent tech for observing the mathematical world : e.g. WL [visualization allow you to humanize what you couldn’t otherwise]

#### We notice pieces of the ruliad that have to do with things like arithmetic and geometry ... and that are modelable/interpretable/observable in those terms

We notice pieces of the ruliad that have to do with things like arithmetic and geometry ... and that are modelable/interpretable/observable in those terms

These come from directly leveraging our physical existence and our physical observer status

#### How far in rulial space have mathematicians managed to go away from our physical observations : i.e. how alien are mathematicians?

How far in rulial space have mathematicians managed to go away from our physical observations : i.e. how alien are mathematicians?

Have mathematicians been the most distant travelers in rulial space?

#### If a mathematician is far away in rulial space ... there’s a reason why nobody cares

If a mathematician is far away in rulial space ... there’s a reason why nobody cares

Because nobody shares that worldview...

#### [Physical observations are our common experience]

[Physical observations are our common experience]

In the future UIs are also common experience [[ e.g. hyperlinks are common experience ]]

< Networks became understood >

## The Continuum Hypothesis

The Continuum Hypothesis

Qualitative idea: if there is an intermediate set, then this is something that the proof process could lead you into ... but if there is no such set, then the proof process can’t leak into the weirdness of the intermediate case ... and it’s always just integers or reals....

(Possibly related to intermediate degrees)

#### Does falsity of the continuum hypothesis imply that you could be in the hyperruliad?

Does falsity of the continuum hypothesis imply that you could be in the hyperruliad?

#### Is CH findable in the ruliad, or do you have to go to the hyperruliad?

Is CH findable in the ruliad, or do you have to go to the hyperruliad?

#### [[It’s a question of what you “notice”]]

[[It’s a question of what you “notice”]]

[[If you don’t notice anything intermediate between integers and reals]]

## Math Genealogy vs Branchial Space

Math Genealogy vs Branchial Space

Genealogical graph of mathematicians is also a multiway graph

Natural foliation of that multiway graph is physical time

### Citation network of mathematics will be similar

Citation network of mathematics will be similar

[ Bibliometric graph ]