Can you explain a bit more *why* the formalist should expect blowups? Just on a sort of semantically blind graph model, it seems to me that fixable proofs should be expected in a system thats both consistent and strongly interconnected. True statements would generally have many possible proofs, and a gap in a proof is also proof-shaped.
For the case where a small additional restriction is needed, the key is that theres some set of cases which werent considered before the error is discovered. So the revealed error doesnt break much, because the theorem was only used for the type of cases that *were* considered. If someone had used a case outside that, they would have already run into a contradiction soon after, and from that the error would have been discovered, before too much is built on the actually false part of the theorem.
This is again predictable from strong connectivity: Most false statements would lead you to a contradiction quickly. If one does not, this is likely because there is a bottleneck between the error and falsum that somehow wasnt crossed yet, and such a bottleneck obviously becomes less likely as you get further away from the false theorem.
The impressive part, if anything, is that a system *can* be so connected and still consistent.
1/ you'd have no way of knowing if the statement is true (in the case of a broken proof) and no way of knowing that a "similar" statement is true (in the case of a broken theorem)
2/ in Neeman's example, you'd expect to have massive spillover from 40 years of relying on a false theorem.
Just imagine that, instead of being driven by intuitive humans, math research was produced by greedy machine-learning algorithms optimizing for maximal productivity. In this scenario, you would never be able to survive 40 years of error.
Its true that you need some way of guessing that statement are true before proof for 1) to work, but its flexible what that is. In the case of Fermats last theorem for example, it has strong inductive support, and had it long before we had any intuition for elliptic curves.
As for 2), I think you didnt understand me. I think even greedy algorithms wouldnt have their house collapse after 40 years. The reason the mistake survived so long is that we never actually reasoned outside the restrictions that needed to be added to the theorem, and that also explains why its an easy fix - just add the restriction to everything that follows, and nothing really changes.
If a machine thought differently from us, and didnt just stick to the area where the theorem really does work, then it would very quickly derive False, and then the problem is noticed, and it doesnt have time to build up 40 years of error. Basically, the only realistic way you can even miss the error for 40 years, *is* by not stepping outside the restrictions.
My point is that, regardless of how you search for proofs, the scenario where it takes 40 years AND a lot WAS built on the error is astronomically unlikely. A search method can make it take 40 years, or it can build on the error a non-tiny amount, but not both. So the lack of blowup isnt much evidence.
There may be a separate argument that it taking 40 years, by itself, points to intuition. I agree this excludes certain types of machines, but it could still happen to semantically blind methods if they are more depth-first.
Adding on to Michael Rosen's point, absent a conjecture that falls into Godel's Incompleteness trap, their either is a proof or there is a counter example to the conjecture. So if the conjecture is true, then there will be a proof - (again, modulo Godel). So there is essentially zero surprise that a proof of a true conjecture can be fixed, although the amount of fixing might be so extensive as to require constructing an entirely new route. Would you agree?
There are different formalisms: ZFC, calculus of constructions (such as Lean), etc. Those formalisms are designed to allow for mathematical proofs. So it is not surprising that they work.What's interesting is that the human brain must also have some sort of neural formalism to allow it to do logic. Whether that neural formalism is learned or partly learned is interesting. What's also interesting is that the brain's neural formalism seems to easily chunk deductions together. That's why Tao says that doing proofs via Lean is about 10x more work than doing it on paper. What is it about the neural formalism that seems to be able to chunk without needing to go through a bunch of tedious steps?
"So if the conjecture is true, then there will be a proof "
Yes, but no. A fixed proof isn't another proof—it's a *similar* proof, fixed. A fixed theorem isn't another theorem—it's a *similar* theorem, fixed. This similarity is the smoking gun of conceptual thinking.
Thanks for your comment that makes me realize this key aspect isn't made explicit in my article—I'll fix it ASAP.
Your writing in Mathematica convinces me. Mathematics is a practice, embedded in an ancient tradition, in the sense described by Alasdair MacIntyre in his book After Virtue. It is best done for the "goods internal to itself" that it provides it's practitioners, and makes them better people as a result. This happens, quite possibly, through the neuroplasticity it augments and facilitates, as you wrote. Providing proof is an integral part of the practice, like a virtue such as honor or justice. It is something that mathematics practitioners strive for, but often fall short of. The flawless proof is an ideal. And forming and holding ideals is a human process, though the content is forever unrealizable and unattainable.
Really great post! But I've got a question; if math is really conceptual, and errors are localized (not spreading everywhere), and we can fix proofs by referring to our intuitive concepts... then why do we need these ultra formal axiom systems like ZFC? What's the point?
We need axioms to *ground* intuition. Formalization within logical consistent system is very specific cognitive device that filters out what our imagination should focus on and channels our learning in the right direction.
I think I see what you mean now. Would it be fair to refine it slightly; axioms don't so much ground intuition as sharpen and constrain it?
My hesitation with 'ground' is that it suggests we build mathematics up from axioms; but as your (great) article shows, thats not really how it works in practice! Most mathematicians (seem to) work with concepts and intuitions directly, not from axiomatic first principles.
Like, the intuition comes first (historically and psychologicaly), but axioms serve as guardrails that; filter out inconsistencies, focus attention on productive structures, enable precise communication. So it's more of a feedback loop than a foundation?
Intuition -> formalization -> refined intuition -> new formalizations... Does that capture what you meant?
Yes. It's a constant back and forth until everything becomes trivial and notation becomes transparent (like we experience it with 2+2=4, which wasn't trivial at all 100 000 years ago.)
“any mathematical theory containing a single contradiction instantly disintegrates into a giant atomic cloud of nonsense, where every statement is both true and false.” So it could be that the universe was created by a fly in Brundle’s machine? Making it a Schrödinger's box in which we are trapped forever more? Cue Rod Serling.🤯
Great observation! It's indeed curious that math proofs are flexible enough that they can be salvaged when broken.
> there isn’t much difference between a proof, a computation, or a theorem
Remembering that proofs are a lot like computations makes this a bit less surprising. After all, your average Python program implementing a complex algorithm can also be in a broken state, yet it can be debugged while keeping most of it intact.
For example, I can be pretty certain that a route exists between my house and my favorite restaurant. Someone says “There’s a shortcut if you skip the highway and take a left at Main Street instead.” It turns out that the shortcut leads to a dead end, and everyone I gave these directions to gets mad at me. That doesn’t change the truth that there does exist route.
It seems like math can still he internally consistent (and a theorem true) even if some of the shortcuts turn out not to be consistent.
Or am I misreading?
Btw - I enjoyed your Econtalk episode, which pointed me to your Substack.
Thank! Yes, many mathematicians describe proof-writing as the process of sequentially describing a landscape that exists in their head and that isn't naturally linear. The description might be wrong, but the landscape is still there.
Interesting. I think that's where it gets to your point on it being Conceptual or Platonic.
I recall a Computer Science theory professor saying "A proof is that which is convincing." (Proof as communication tool. It may be formally correct but if it can't convince then it's not useful.)
I don't get the point of this piece. The reason proofs are fixable is obvious.
If a proof has the form A->B->C->D->E->F->Theorem
and we notice that D actually doesn't imply E we still have all our five other implications.
If we imagine a very unrealistic world where each step has an equal probability (p) of being true, then proving a theorem of this length requires luck on the order of p^6, but fixing it will have a much higher rate of success, p.
I have been thinking a lot about this question recently too, and I have come to a view of math that I call "computational platonism" (https://arxiv.org/abs/2506.19787). Briefly, we make precise definitions of computational systems (like the natural numbers with a successor operation and addition/multiplication). These are a physical process and we have to compute to know what's happening - they are what take the place of physical experiments. And in fact, they are a very particular kind of physical experiment.
But there is a second step, where we notice patterns in these computational systems (like the commutativity of addition or the inductive principle) and we formulate axiom systems that encode some of these symmetries we observe, and from them we try to deduce others. In this way, our axiomatics frameworks are much more like the general theory of relativity (a conjectured description of reality) than anything else. And correspondingly, a "contradiction" in mathematics is merely us having failed to find a sufficiently correct general theory.
Note that the basic computational procedure cannot have contradictions - the idea makes no sense in that context! The physical world cannot have a contradiction, it can only be in our heads. Mathematics has at least two more interesting twists over physics.
1) We get to define new computational systems, and we often choose these new systems to extract some essential pattern out of the older ones we care about (but not always). This is often a hugely creative part of mathematics.
2) Turing completeness is both a curse and boon. Most of our computational frameworks are bi-interpretable in principle (but in practice, there are huge differences of course). But conversely, Godel incompleteness guarantees us that any computational framework of sufficiently interesting reality will be incomplete. In some sense, this is parallel to how physical experiment can never confirm a physical theory, only disprove it.
So the platonism is in our heads, because we refine our computational systems to move closer to the picture we develop in our head based on actual computational experiences (construed broadly).
And the reason mathematics is resistant to local errors is that we are always trying to describe the base computational system and a false theorem is only a false description of reality. If it's "sufficiently false", we will notice a contradiction quickly from practice, and if we don't notice a contradiction in practice, it's because the "false theorem" was still describing some true aspect of reality.
Happy to hear your thoughts, I have never quite seen the above view laid out and I think it explains a lot of my own experience as a working mathematician.
Through my framework, this "fix" is math meeting the way cognition works. Not to be disrespectful for such great mathematicians but it is converging to the way we operate. And seeing that the mathematics is pretty much nowadays about shapes, correspondences and representational spaces. https://eworks77.substack.com/p/ontowards-a-rosetta-stone
Meaningless symbols acquire meaning by convention. Then symbols start referring to concepts - abstract filters for a broad context, be it in front of one's eyes, in memory, or in imagination. Filters rely on properties, more specifically on ranges of properties. In terms of properties, objects are multidimensional. Against any property, they fall into different ranges. Ranges may be consecutive (like [0, 9], [10, 19] ...) or rule-based (odd vs even numbers, prime vs composite numbers, etc.). Filters can be stacked to refer to one or more specific objects in the given context. Apply one filter to the context and many objects pass through. Apply an additional filter to the result and a new resulting subset is yet smaller or even empty. Venn diagrams are one example. The game 20 Questions is another. Language references work this way. Intelligence works this way. My whole Substack is about "this way."
Can you explain a bit more *why* the formalist should expect blowups? Just on a sort of semantically blind graph model, it seems to me that fixable proofs should be expected in a system thats both consistent and strongly interconnected. True statements would generally have many possible proofs, and a gap in a proof is also proof-shaped.
For the case where a small additional restriction is needed, the key is that theres some set of cases which werent considered before the error is discovered. So the revealed error doesnt break much, because the theorem was only used for the type of cases that *were* considered. If someone had used a case outside that, they would have already run into a contradiction soon after, and from that the error would have been discovered, before too much is built on the actually false part of the theorem.
This is again predictable from strong connectivity: Most false statements would lead you to a contradiction quickly. If one does not, this is likely because there is a bottleneck between the error and falsum that somehow wasnt crossed yet, and such a bottleneck obviously becomes less likely as you get further away from the false theorem.
The impressive part, if anything, is that a system *can* be so connected and still consistent.
The issues are:
1/ you'd have no way of knowing if the statement is true (in the case of a broken proof) and no way of knowing that a "similar" statement is true (in the case of a broken theorem)
2/ in Neeman's example, you'd expect to have massive spillover from 40 years of relying on a false theorem.
Just imagine that, instead of being driven by intuitive humans, math research was produced by greedy machine-learning algorithms optimizing for maximal productivity. In this scenario, you would never be able to survive 40 years of error.
Its true that you need some way of guessing that statement are true before proof for 1) to work, but its flexible what that is. In the case of Fermats last theorem for example, it has strong inductive support, and had it long before we had any intuition for elliptic curves.
As for 2), I think you didnt understand me. I think even greedy algorithms wouldnt have their house collapse after 40 years. The reason the mistake survived so long is that we never actually reasoned outside the restrictions that needed to be added to the theorem, and that also explains why its an easy fix - just add the restriction to everything that follows, and nothing really changes.
If a machine thought differently from us, and didnt just stick to the area where the theorem really does work, then it would very quickly derive False, and then the problem is noticed, and it doesnt have time to build up 40 years of error. Basically, the only realistic way you can even miss the error for 40 years, *is* by not stepping outside the restrictions.
"The reason the mistake survived so long is that we never actually reasoned outside the restrictions that needed to be added to the theorem"
This happened *precisely* we only operated within the "meaningful" region of deductive reasoning, and never ventured into the "greedy" part.
The important fact is that it took 40 years AND it was no big deal. With a greedy machine, you can't have both outcomes together.
My point is that, regardless of how you search for proofs, the scenario where it takes 40 years AND a lot WAS built on the error is astronomically unlikely. A search method can make it take 40 years, or it can build on the error a non-tiny amount, but not both. So the lack of blowup isnt much evidence.
There may be a separate argument that it taking 40 years, by itself, points to intuition. I agree this excludes certain types of machines, but it could still happen to semantically blind methods if they are more depth-first.
Adding on to Michael Rosen's point, absent a conjecture that falls into Godel's Incompleteness trap, their either is a proof or there is a counter example to the conjecture. So if the conjecture is true, then there will be a proof - (again, modulo Godel). So there is essentially zero surprise that a proof of a true conjecture can be fixed, although the amount of fixing might be so extensive as to require constructing an entirely new route. Would you agree?
There are different formalisms: ZFC, calculus of constructions (such as Lean), etc. Those formalisms are designed to allow for mathematical proofs. So it is not surprising that they work.What's interesting is that the human brain must also have some sort of neural formalism to allow it to do logic. Whether that neural formalism is learned or partly learned is interesting. What's also interesting is that the brain's neural formalism seems to easily chunk deductions together. That's why Tao says that doing proofs via Lean is about 10x more work than doing it on paper. What is it about the neural formalism that seems to be able to chunk without needing to go through a bunch of tedious steps?
"So if the conjecture is true, then there will be a proof "
Yes, but no. A fixed proof isn't another proof—it's a *similar* proof, fixed. A fixed theorem isn't another theorem—it's a *similar* theorem, fixed. This similarity is the smoking gun of conceptual thinking.
Thanks for your comment that makes me realize this key aspect isn't made explicit in my article—I'll fix it ASAP.
Fix done, added final paragraph on that.
Kintsugi to the rescue!
Glad someone noticed the self-reference :)
“There is a crack, a crack in everything
That's how the light gets in” -Leonard Cohen
Your writing in Mathematica convinces me. Mathematics is a practice, embedded in an ancient tradition, in the sense described by Alasdair MacIntyre in his book After Virtue. It is best done for the "goods internal to itself" that it provides it's practitioners, and makes them better people as a result. This happens, quite possibly, through the neuroplasticity it augments and facilitates, as you wrote. Providing proof is an integral part of the practice, like a virtue such as honor or justice. It is something that mathematics practitioners strive for, but often fall short of. The flawless proof is an ideal. And forming and holding ideals is a human process, though the content is forever unrealizable and unattainable.
Really great post! But I've got a question; if math is really conceptual, and errors are localized (not spreading everywhere), and we can fix proofs by referring to our intuitive concepts... then why do we need these ultra formal axiom systems like ZFC? What's the point?
Thanks for the feedback!
We need axioms to *ground* intuition. Formalization within logical consistent system is very specific cognitive device that filters out what our imagination should focus on and channels our learning in the right direction.
Thanks for the clarification!
I think I see what you mean now. Would it be fair to refine it slightly; axioms don't so much ground intuition as sharpen and constrain it?
My hesitation with 'ground' is that it suggests we build mathematics up from axioms; but as your (great) article shows, thats not really how it works in practice! Most mathematicians (seem to) work with concepts and intuitions directly, not from axiomatic first principles.
Like, the intuition comes first (historically and psychologicaly), but axioms serve as guardrails that; filter out inconsistencies, focus attention on productive structures, enable precise communication. So it's more of a feedback loop than a foundation?
Intuition -> formalization -> refined intuition -> new formalizations... Does that capture what you meant?
Yes. It's a constant back and forth until everything becomes trivial and notation becomes transparent (like we experience it with 2+2=4, which wasn't trivial at all 100 000 years ago.)
This has been the topic of a long and popular MathOverflow thread: https://mathoverflow.net/questions/338607/why-doesnt-mathematics-collapse-even-though-humans-quite-often-make-mistakes-in . But some broken theorems have stayed broken for a long time, while others remain so even now: https://mathoverflow.net/questions/257628/theorems-demoted-back-to-conjectures .
NB: the fix to the divided powers bug is still not published. Mathematics's self-healing powers are remarkable but also remarkably slow.
Thanks for the links!
Yes, the self-healing process is quite slow—the truly striking aspect is that it's still OK, as fracture lines don't propagate monstrously far.
Mathematics is an empirical science.
I meant to cite this brilliant paper from Von Neumann
https://prclare.people.wm.edu/m150s21/vonNeumann.pdf
which is much deeper than my sentence.
“any mathematical theory containing a single contradiction instantly disintegrates into a giant atomic cloud of nonsense, where every statement is both true and false.” So it could be that the universe was created by a fly in Brundle’s machine? Making it a Schrödinger's box in which we are trapped forever more? Cue Rod Serling.🤯
Great observation! It's indeed curious that math proofs are flexible enough that they can be salvaged when broken.
> there isn’t much difference between a proof, a computation, or a theorem
Remembering that proofs are a lot like computations makes this a bit less surprising. After all, your average Python program implementing a complex algorithm can also be in a broken state, yet it can be debugged while keeping most of it intact.
Very interesting post.
Is one analogy for the process driving?
For example, I can be pretty certain that a route exists between my house and my favorite restaurant. Someone says “There’s a shortcut if you skip the highway and take a left at Main Street instead.” It turns out that the shortcut leads to a dead end, and everyone I gave these directions to gets mad at me. That doesn’t change the truth that there does exist route.
It seems like math can still he internally consistent (and a theorem true) even if some of the shortcuts turn out not to be consistent.
Or am I misreading?
Btw - I enjoyed your Econtalk episode, which pointed me to your Substack.
Thank! Yes, many mathematicians describe proof-writing as the process of sequentially describing a landscape that exists in their head and that isn't naturally linear. The description might be wrong, but the landscape is still there.
Interesting. I think that's where it gets to your point on it being Conceptual or Platonic.
I recall a Computer Science theory professor saying "A proof is that which is convincing." (Proof as communication tool. It may be formally correct but if it can't convince then it's not useful.)
I don't get the point of this piece. The reason proofs are fixable is obvious.
If a proof has the form A->B->C->D->E->F->Theorem
and we notice that D actually doesn't imply E we still have all our five other implications.
If we imagine a very unrealistic world where each step has an equal probability (p) of being true, then proving a theorem of this length requires luck on the order of p^6, but fixing it will have a much higher rate of success, p.
I have been thinking a lot about this question recently too, and I have come to a view of math that I call "computational platonism" (https://arxiv.org/abs/2506.19787). Briefly, we make precise definitions of computational systems (like the natural numbers with a successor operation and addition/multiplication). These are a physical process and we have to compute to know what's happening - they are what take the place of physical experiments. And in fact, they are a very particular kind of physical experiment.
But there is a second step, where we notice patterns in these computational systems (like the commutativity of addition or the inductive principle) and we formulate axiom systems that encode some of these symmetries we observe, and from them we try to deduce others. In this way, our axiomatics frameworks are much more like the general theory of relativity (a conjectured description of reality) than anything else. And correspondingly, a "contradiction" in mathematics is merely us having failed to find a sufficiently correct general theory.
Note that the basic computational procedure cannot have contradictions - the idea makes no sense in that context! The physical world cannot have a contradiction, it can only be in our heads. Mathematics has at least two more interesting twists over physics.
1) We get to define new computational systems, and we often choose these new systems to extract some essential pattern out of the older ones we care about (but not always). This is often a hugely creative part of mathematics.
2) Turing completeness is both a curse and boon. Most of our computational frameworks are bi-interpretable in principle (but in practice, there are huge differences of course). But conversely, Godel incompleteness guarantees us that any computational framework of sufficiently interesting reality will be incomplete. In some sense, this is parallel to how physical experiment can never confirm a physical theory, only disprove it.
So the platonism is in our heads, because we refine our computational systems to move closer to the picture we develop in our head based on actual computational experiences (construed broadly).
And the reason mathematics is resistant to local errors is that we are always trying to describe the base computational system and a false theorem is only a false description of reality. If it's "sufficiently false", we will notice a contradiction quickly from practice, and if we don't notice a contradiction in practice, it's because the "false theorem" was still describing some true aspect of reality.
Happy to hear your thoughts, I have never quite seen the above view laid out and I think it explains a lot of my own experience as a working mathematician.
Through my framework, this "fix" is math meeting the way cognition works. Not to be disrespectful for such great mathematicians but it is converging to the way we operate. And seeing that the mathematics is pretty much nowadays about shapes, correspondences and representational spaces. https://eworks77.substack.com/p/ontowards-a-rosetta-stone
Meaningless symbols acquire meaning by convention. Then symbols start referring to concepts - abstract filters for a broad context, be it in front of one's eyes, in memory, or in imagination. Filters rely on properties, more specifically on ranges of properties. In terms of properties, objects are multidimensional. Against any property, they fall into different ranges. Ranges may be consecutive (like [0, 9], [10, 19] ...) or rule-based (odd vs even numbers, prime vs composite numbers, etc.). Filters can be stacked to refer to one or more specific objects in the given context. Apply one filter to the context and many objects pass through. Apply an additional filter to the result and a new resulting subset is yet smaller or even empty. Venn diagrams are one example. The game 20 Questions is another. Language references work this way. Intelligence works this way. My whole Substack is about "this way."