Below are some of my reflections on the nature of proof in the age of proof abundance (due to LLMs). Those ruminations have been cleaned up, compiled, and stitched together with the aid of an LLM.
Imagine two mathematicians trying to prove the same theorem. The first works through 150 steps. None is mysterious; each follows correctly from what came before. Yet the argument, taken as a whole, is difficult to hold in mind. The second mathematician spots something else: the theorem is a special case of a much more general result. With that observation, the proof takes three lines.
Which proof is more insightful?
The tempting answer is the second. We admire proofs that replace calculation with insight, a thicket of details with a single clear idea. But this judgment may tell us as much about the minds doing the judging as about mathematics itself.
A mathematical proof must meet standards of validity. A mathematical explanation must also meet a reader. And different readers—and perhaps different kinds of intelligence—have very different capacities for finding, following, and organizing chains of reasoning.
To see why this matters, imagine an abstract space of mathematical facts. Across this space lie various enclosed regions, each associated with a particular mathematical idea. Some are large, others small. Some overlap considerably, while others appear isolated. Their shapes need not be regular. One region might represent mathematical induction, another the concept of an invariant, another a powerful theorem connecting two previously separate fields.
We can think of these regions as closed sets, representing the scope of mathematical consequences made readily accessible by particular ideas.
These are not simply sets of everything that follows logically from an idea. They are regions of *mathematical intelligibility*: results that a trained mathematician can recognize as natural consequences, without having to rebuild the argument from scratch. Near the conceptual centre of a region, the implications seem obvious. Toward its boundaries, they require ingenuity. And those boundaries are not entirely sharp, because familiarity, ingenuity, and background knowledge vary from person to person.
The same theorem might lie near the outer limit of one region and comfortably within another. What looks like a distant and difficult destination from one mathematical vantage point can be almost underfoot from another.
Now imagine the two mathematicians again. The second notices that the theorem belongs to the region illuminated by an established principle. Her achievement is not merely reaching the theorem; it is recognizing where the theorem belongs. She finds a place for it within a broader mathematical structure.
The first mathematician begins elsewhere. He crosses the spaces between familiar conceptual regions, moving from one justified inference to the next. He has found a path, but not necessarily a panoramic view of the terrain. His proof may be formidable, meticulous, and entirely correct without being easy to describe as one overarching idea.
These are two different forms of mathematical understanding. One reveals a theorem's place within a broader conceptual structure. The other establishes a route to it, perhaps from an altogether different mathematical starting point. Neither accomplishment necessarily entails the other.
This distinction offers an interesting perspective on the emerging role of artificial intelligence in mathematics.
Humans have limited working memory. We have learned to cope, in part, by turning complicated procedures into concepts we can carry around as single units: "use induction", "find an invariant", "pass to a quotient". What once demanded a page of reasoning can become one move on the mental chessboard.
AI systems can sometimes approach a problem differently. A language model working with search, external memory, or a proof assistant may explore and check long inferential routes that would be exhausting for a person to discover or survey. That does not make an LLM infallible, and a fluent sequence of claims is not automatically a valid proof. The point is subtler: systems with different cognitive and computational resources may find different routes through the same mathematical territory.
Nor does it follow that AI produces only sprawling arguments, or that humans produce only elegant insights. AI can suggest useful constructions and unexpected connections; mathematicians can labour through hundreds of technical steps. The contrast concerns possible cognitive advantages, not an absolute division between different kinds of intelligence.
Consider a historical thought experiment. Today, an AI system finds a valid but ungainly proof of a difficult theorem, using mathematical ideas that already exist. Twenty years later, an entirely new field has developed. Someone realizes that the old theorem is now an almost immediate consequence of two general principles.
The theorem has not changed. Its truth has not become truer. What has changed is the landscape: new regions of mathematical intelligibility have emerged, making accessible what previously required an arduous deductive journey.
This is why mathematical elegance has a historical dimension. A proof that is transparent to an expert in a mature field may be opaque to a student, and literally unimaginable to a mathematician working before that field existed. We might call this a relativity of *conceptual distance*, without confusing it with a relativity of mathematical truth.
Still, the shorter proof is not automatically the better one. Mathematicians often prize *elementary proofs*: arguments that avoid advanced theoretical machinery, even at the price of considerable length or ingenuity.
Fermat's Last Theorem, for example, was finally proved through deep connections involving elliptic curves and modular forms. No elementary proof is known. Yet one can imagine a different argument proceeding from comparatively elementary number theory, perhaps through hundreds of ingenious deductions. Such a proof could reveal something important that the established proof does not, even if it were considerably longer.
There is another possibility, however, and it changes our mathematical landscape yet again.
Suppose the original 150-step argument begins to recur. Other mathematicians notice that its moves can be adapted to new problems. They name the method, streamline its presentation, and teach it. What once looked like a cumbersome expedition becomes a standard route.
In modal logic, canonical-model constructions illustrate something like this transformation. Students first encounter a formidable apparatus: collections of formulas used to construct "possible worlds", carefully defined relations between those worlds, and an argument connecting the syntactic properties of formulas with truth in the resulting model.
Later, the same student may hear "use the canonical model" and recognize an entire strategy at once. A complicated construction has become a familiar tool. Its internal complexity has not disappeared, but the experienced logician can now handle it as a single recognizable method.
In our conceptual landscape, we could represent this development by introducing a new enclosed region. Unlike a general theorem that places a result neatly within an existing theory, this region may encompass the *deductive route itself*. A lengthy procedure has become familiar enough to function as a mathematical idea in its own right. Its territory may overlap with several older regions, creating connections that were previously difficult to recognize.
Not every long proof undergoes that transformation. Some arguments remain isolated, useful chiefly because they establish the result they set out to prove. Others become standard tools through their versatility, their explanatory power, or their repeated adoption by the mathematical community.
Mathematical ideas, then, do not become familiar in only one way. Some offer immediate conceptual clarity. Others acquire their place in the mathematical toolkit through repeated application and gradual refinement. Familiarity can arise from understanding a general principle, but also from mastering a procedure.
And the regions of our mathematical landscape are not fixed. Their boundaries may shift with education, experience, and the historical development of mathematics. What lies near the limits of one person's mathematical intuition may lie at the very heart of another's.
The prospect of AI-assisted mathematics makes these distinctions more than philosophical curiosities.
We may increasingly encounter theorems for which a rigorous proof is available, but no particularly satisfying conceptual explanation has yet emerged. The work of mathematics would not end there. Researchers could still ask which steps matter most, what general principles lie hidden in the details, and whether the argument opens an entirely new region of mathematical thought.
Indeed, a complicated AI-generated proof might eventually become the basis for a new mathematical idea. Or a future mathematician might discover a completely different proof, rendering the original argument unnecessary for understanding the result. Neither outcome diminishes the original achievement.
The important distinction is between establishing a mathematical truth and finding a conceptual organization that makes it intelligible. These achievements often go hand in hand, but they need not.
And perhaps that is what the arrival of new kinds of mathematical intelligence will help us appreciate.
A proof tells us that a destination can be reached. An idea can show us why the destination belongs within a familiar region of mathematical understanding—or teach us a route worth travelling again.
Mathematics needs both.
Its truths may stay put, but the landscape of what different minds can readily see is always changing.
