This report defines a hole for the proof space arising in multiway system graphs generated by string-substitution rules. A proof is a path from an initial string to a target string (the initial and final string is a theorem) in the graph. By contracting each proof to a single vertex and connecting two proofs when they differ in exactly one step (when they form a single diamond sub-graph), at the end it constructs a proof graph whose connectedness tells the fact of continuously deforming one proof into another. A hole is defined as follows: #Holes = #ConnectedComponents - 1
Adding new symbols or asymmetric rules quickly introduces holes.

Homotopies in multiway system graphs

Goal: We aim to study the process of reaching theorems, not just the theorems themselves. We will do this by directly examining the structure of the proof space.
Consider the rule set {ABBB, BBA} and the theorem AABA. To find all possible proofs, we must first identify a path from A to ABA in the multiway system.
Out[]=
In this particular case, there are 20 distinct paths (also called proofs for this theorem AABA)
Out[]=

,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,

All these different proofs, can in a sense, be continuously deformed into each other. Therefore, we need to define what makes a proof be continuously deformed into another one, in this case we do that by progressively changing just one step at a time . In this case, the proofs are equivalent. This starting point will later serve as a baseline against which finer topological structures on proof space can be compared.
Now consider the rule {A AA, A  BAAB} . With this axiom system, there are 15 possible proofs for the theorem A BAABAABAAB :
The proofs on the left side cannot be continuously deformed into the proofs on the right side. This indicates the presence of a topological “hole” between these two groups of proofs (that is, a non-trivial loop separating the two clusters of proofs).
​Observations: Note that the existence and nature of such holes depend crucially on the particular theorem under investigation.

Brainstorm

Defining “no holes” and “holes” in the proof space

Out[]=
Out[]=
The main task is to define precisely what it means for the proof space to have a hole. Before studying the theorem A
⟹
BAABAABAAB, we begin by examining a simpler theorem: A
⟹
BAABAA, for which we want to prove that no holes exist in its proof space. In this case, there are only two distinct proofs for the theorem. We contract each path into a single node to build a new graph the proof graph for this theorem (the graph of every possible proof for the theorem). We then define an edge between two nodes if the corresponding proofs differ by exactly one diamond.
​
The resulting graph may be connected, or disconnected. If it is connected we say that the topological space of proofs for this theorem has no holes, meaning every proof could be continuously deformed into any other. Essentially, the proof space is path-connected and can be considered as having a single equivalence class of proofs.
​
On the other hand, if the graph is disconnected, this indicates the presence of a hole in the proof space, separating distinct classes of proofs.
​
At the end this would be the resulting graph for the theorem A
⟹
BAABAA.
Out[]=
And now we have a first definition to count the number of holes in a theorem: metatheorem: (#Holes) = (#connected components) - 1
Let' s look at the next example whose rule is {ABBB, BB  A} and think about the theorem A
⟹
AA.
Out[]=
In[]:=
A=Withg=
[◼]
TwoWayRuleStringNestGraph
[{"A"->"BBB","BB"->"A"},"A",6,VertexShapeFunctionAutomatic,EdgeStyleDirective[Arrowheads[.1],Darker[ResourceFunction["WolframPhysicsProjectStyleData"]["StatesGraph","EdgeStyle"]]],AspectRatio->1.5,ImageSize->100],HighlightGraphg,StylePathGraph[#,DirectedEdgesTrue],
[◼]
MetamathematicsStyleData
["ProofPathStyle"],Thickness[0.03]&/@FindPath[g,"A","AA",All,All]

P1,
P2,
P3,
P4
There are four different proofs for this theorem. Look at the first two paths P1 (red), P2 (blue) and overlap them in different colors:
Out[]=
Note that the two paths draw a diamond (BBBB,BBA,AA,ABB):
Out[]=
So the two paths P1,P2 are contracted in two nodes and since they form only one diamond. In the resulting graph they are connected:
Do the same with the other proofs P3 (green), P4 (Orange) and overlap them in different colors:
And by doing the same process with P4,P2 and P1,P3 we complete the graph:
Then convert every path into a node and construct the edges by using the relation “two paths are connected if the proofs are different in only one step”. And we obtain the graph, which only has a connected component, then this theorem has no holes. It is amazing that the new graph is telling us which is the metapath to go from one proof to another one continuously.
This is the resulting graph after applying the algortim, #holes = #ConnectedComponents - 1 = 2-1=1. So this theorem, actually, as we have thought has a hole.

The easiest hole

So far, we haven’t seen an example of a theorem without holes, because it is a bit harder to find a graph that contains a hole (a theorem for which at least one proof cannot be converted into another by switching at most one step). To understand what a hole looks like, we will take a shortcut and show the simplest graph (which does not come from a rule) that contains a hole.

Spreading the concept

Once we have defined what the meaning of a hole in a theorem means, we can search for holes in graphs by searching for every possible theorem in a graph and computing how many theorems have holes (and how many holes they have).

Interpretation and application

Pythagorean theorem

1st Proof of Pythagorean theorem (side ratios, geometry) P1

2nd Proof of Pythagorean theorem (area rearrangement, geometry) P2

3rd Proof of Pythagorean theorem (distance formula) P3

Let’s see how pythagorean theorem is represented by using graphs. The proof space for the Pythagorean theorem is:
Then, by using the algoritm we developed before, we have that the resulting graph is:
We conclude that, if we only use these three proofs, the pythagorean theorem has 2 holes.

Main results and examples

Example of graphs whose theorems have no holes

Let’ s analyze a simple example: let the rule be {AB, B  AA} and let’s start the graph at A. Note that we have only two rules and the initial condition is just one letter, “A”. We apply the rules 7 times. Notice that the graph generates every possible theorem (there are 5 possible theorems) and every possible proof. Then, we apply the algorithm to determine how many holes each theorem has. In the end, we see that the number of holes in every theorem is zero. The “density” of the graph increases each time we apply the rules, so we will never find a hole.
In the next example we are giving again the same two rules but this time the initial conditions are two letter “AB”, and we are applying the rule 7 times, note again that the “density” of the graph becomes bigger very fast once again, so we are never going to find a hole.
These are the resulting graphs after applyng the algorithm

Example of graphs whose theorems have holes

Let’s make a hole, we give two rules {ABB, B  AA} with initial condition “ABA”, note that holes begin to appear by applying the rule five times.
Now begin with three rules {A  BC, B  AA, C  A} (we are adding a new letter) and initial condition of only one letter, let’s apply the rule seven times
Now three rules but this time {A  BC, B  AA, C  A}, the initial condition is one letter longer

Concluding Remarks

An important observation is that we can begin formulating metatheorems—statements about the structure of the proof space itself. For instance: given any set of two or more rewriting rules, there exist a natural number 𝑛 and an appropriate initial condition such that the resulting proof space contains holes.

Acknowledgments

First of all I would like to say that I am very grateful to Stephen Wolfram for proposing this research topic. At first, I was worried about not being able to meet the expectations, but it was great to know that Stephen was satisfied with the result. I would like to thank also Hugo Suárez and Alejandra Ortiz for their support throughout the development of this notebook. I deeply appreciate their time. This notebook would not have been possible without their help.

References

1
.
S. Wolfram (2022), “The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics” Wolfram Science. https://www.wolframscience.com/metamathematics/.
2
.
Ž. Virk, (2022), Introduction to Persistent Homology. University of Ljubljana.

Cite This Notebook

Searching for holes in the proof space​
by Saúl Bernal González​
Wolfram Community, Staff Picks, July 9, 2025
​https://community.wolfram.com/groups/-/m/t/3497454