Can AI Write Mathematical Proofs That Humans Cannot Understand?

When AI's Proofs Exceed Human Understanding

A rather counterintuitive idea came up on the Lex Fridman podcast: if an AI produces a mathematical proof that baffles every expert in the field—not because it is too long, but because the ideas in it are incomprehensible—what should humans do?

The interlocutor's answer carried a logician's coolness: there are only a handful of inference rules, and only a handful of axioms. Under these constraints, the only way to produce "incomprehensible mathematics" is almost certainly scale. In other words, the threshold for understanding can be raised, but the underlying grammar of mathematics remains finite.

This judgment itself is worth pondering. It pulls "incomprehensibility" back from mysticism into an engineering problem—not that mathematics has turned into magic, but that the search space has grown so vast that human cognition struggles to reconstruct it within a finite time.

The Tension Between Formalization and Intuition

The conversation raised a "reverse" question: what would unformalizing mathematics look like? Formalization gives humans confidence in the correctness of results, but the way humans understand a result largely remains at the informal level—what counts as an interesting special case? Where does this technique come from? What problems does it parallel?

This leads to two things that are often conflated: the engineering of the proof and the communication of that to someone else. The interlocutor pointed out that when writing a paper, these two are almost opposites. Engineering pursues rigor; communication pursues a tangible narrative.

A "Reverse-Order" Experiment in a Real Analysis Course

The interlocutor shared his experience teaching real analysis. Any real analysis textbook begins by constructing the real numbers—defining them as equivalence classes of Cauchy sequences of rationals, spending about two weeks on it, then returning to the number line and starting ε-δ calculus. His question was: before the course, students already know what real numbers are—it's that number line; two weeks later the number line comes back. What was the point of those two weeks in between?

His approach was to teach it in reverse: dive straight into ε-δ computations, do them for six weeks, until hitting the Bolzano–Weierstrass theorem—every bounded sequence of real numbers has a convergent subsequence. This theorem does not hold for rationals but does for reals. Why? What exactly are real numbers? Only at this point do students genuinely ask the construction question.

This is precisely the divide between "telling" and "constructing." If the goal is to build a theory, you must first construct the objects; if the goal is to tell a story, you can start entirely from intuition until intuition hits a wall.

The Bolzano–Weierstrass theorem is one of the fundamental theorems in real analysis: every bounded infinite sequence in the real numbers ℝ contains a convergent subsequence (whose limit is also in ℝ). It is used as a key node in teaching because it reveals the essential difference between the real number system and the rational number system—the same proposition fails on ℚ; for example, a bounded sequence of rational approximations to √2 does not converge in ℚ. The theorem's validity depends on the completeness of the reals (the least upper bound property), and completeness is exactly the core property that the Cauchy sequence construction of the reals is meant to guarantee. Thus, when students "hit the wall" on this theorem, the reverse-order teaching naturally leads them back to the construction question of "what exactly are real numbers"—this is precisely the intent behind the interlocutor's teaching path.

Mathematics Is Not the Rising Tide of Theorems

The interlocutor explicitly rejects a view of mathematics: that mathematics is simply a continuous increase in the number of theorems, so how could AI contributing theorems be harmful? His rebuttal is that mathematics is far more than a count of theorems; it also includes the process of wrestling with problems.

A good problem fights back. In the struggle, researchers discover more general meaning and build a system of beliefs and abstractions. This system is the substantial part of mathematics, and theorems are merely its slices at some coordinate.

From this follows a judgment about writing in the AI era: the form of future papers will be very different—more space devoted to telling "what I learned along this path": the standard steps here and there, where the sticking points appeared, why we chose to go left rather than some other direction; along with a streamlined formalization to ensure the engineering holds up.

The story cannot exist alone. Mathematics is not music; it cannot bypass the rules with beautiful parallel voices—Bach could do that, mathematics cannot.

"Problems fighting back" in mathematics can be understood by comparing with classic cases in the history of mathematics. Hilbert's 23 problems proposed in 1900, the Weil conjectures, and the Langlands program have all reshaped entire fields by "fighting back": tools invented to solve a problem (such as ideals, sheaves, cohomology) are often more important than the solution to the original problem. This is consistent with what the interlocutor said about "wrestling with problems producing more general abstractions." In other words, the substantial growth of mathematics often manifests as the expansion and reorganization of conceptual systems, and the number of theorems is merely the projection of this expansion at the formal level. Understanding this makes it clear why "AI producing more theorems" does not automatically equate to "progress in mathematics."

Black-Box Proofs and the Second Outsourcing of Understanding

Back to the original question. If AI produces a proof that humans cannot read, one pragmatic path is: have another LLM explain the story, break the proof into smaller questions that are easier to probe, and gradually rebuild understanding of "how exactly did it arrive at the answer."

There is an implicit hierarchy here: a proof can be verified line by line and still not be understood. Verification and understanding are not the same thing. The interlocutor repeatedly emphasized that what humans want is the story, is understanding, not just a certificate of correctness.

This also explains why the answer "scale" is both valid and unsatisfying. Scale can explain why a proof exceeds human reconstruction capacity, but it cannot explain why humans still insist on telling it as a story. And the latter is precisely the part of mathematics as a human endeavor.

The difference between formal verification and understanding has a clear counterpart in the foundations of mathematics. A formal proof is a string of symbols conforming to inference rules, which can be verified line by line by a computer (as proof assistants like Lean and Coq do); but "understanding" involves grasping at the semantic level—why does this proof hold, where do the key lemmas come from, which step carries the substantial idea. Logic has long distinguished: a proof can be valid (formally correct) without necessarily being intelligible. Research in proof theory after Gödel's incompleteness theorems also shows that there is no necessary equivalence between formal verifiability and human reconstructability. This is precisely the technical background for the interlocutor's statement that "verification and understanding are not the same thing."

Some Sober Reflections on AI Mathematics

Putting this conversation back into the current discussion of AI mathematics, there are several judgments worth remembering.

First, the value of formal verification will rise as AI output increases, but formalization is not the endpoint; it is merely the minimum guarantee that makes the engineering trustworthy.

Second, AI's real contribution to mathematics may not lie in the number of theorems, but in whether it can provide intermediate narratives that humans can absorb—which special cases are worth looking at, why a particular path was abandoned. This kind of "process knowledge" is still scarce.

Third, the metaphor of "wrestling with problems" points to a cognitive activity that is hard to outsource. The moment a problem fights back is the moment a new abstraction is born. If AI skips the struggle and gives the answer directly, what humans get may be correct but ungrowable knowledge.

The conversation did not provide a final answer, but it advanced the question from "can AI do mathematics" to "what exactly is the mathematics humans want." This shift itself is more valuable than any single conclusion.

One-line Summary

If AI produces proofs humans cannot understand, verification is not understanding; the essence of mathematics is the process of wrestling with problems.

Paragraph Summary

Starting from an idea on the Lex Fridman podcast: if AI produces a mathematical proof that even experts cannot understand, what should humans do? The interlocutor believes that because the number of inference rules and axioms is finite, the only way to produce "incomprehensible mathematics" is almost certainly scale. The article then distinguishes between the engineering of a proof and its communication, using a "reverse-order" real analysis teaching example to illustrate the divide between telling and constructing. The author rejects the view that "mathematics is just a rising count of theorems" and emphasizes that the essence of mathematics is the process of wrestling with problems and producing more general abstractions. Facing black-box proofs, a viable path is to use another LLM to deconstruct the narrative and rebuild human understanding of where the answer comes from. Ultimately, the article points out that the value of formal verification will rise but is not the endpoint; AI's true contribution may lie in providing absorbable intermediate narratives.