Abstract
Recent AI-generated mathematical results have revived questions about the relationship between proof, understanding and mathematical value. This article reconstructs an inquiry that began by welcoming automated discovery and developed into a challenge to the assumption that human intelligibility should determine the boundaries of mathematics. Through an AI-assisted dialogue, close reading of historical and recent mathematical and philosophical work, and examination of a reported local-smoothing proof, I distinguish the difficulty of discovering an argument from the difficulty of verifying, explaining or learning from it. I argue that present opacity does not establish permanent human incomprehensibility, while a failure to understand does not establish mathematical insignificance. The discussion then examines mathematical beauty, computational metamathematics, the attraction and limits of Platonist interpretations, and disputes over access, credit and research direction. Its central proposal preserves human understanding as a major purpose of mathematical institutions without making it a universal condition of mathematical validity. Questions about future machine capabilities, the extent of human cognitive limits and the metaphysical status of mathematics remain open. The inquiry clarifies how these uncertainties require different kinds of evidence and judgement.
Keywords: AI-assisted mathematics; mathematical understanding; formal proof; mathematical aesthetics; computational metamathematics; mathematical realism; epistemic labour.
I began with a question that seemed almost too straightforward to require an argument. If artificial intelligence proves difficult mathematical results, why should mathematicians regard that as a crisis? More mathematics has become available. Problems that resisted years of work may now have solutions. Whatever the disruption to professional expectations, surely this is good for mathematics. Reports of hundreds of AI-generated research manuscripts made the question urgent, although the size of a release cannot tell us how many independent, correct or important advances it contains (Calegari, 2026).
The question became less straightforward when I read Luo Xincheng’s discussion of the difference between a mechanically verifiable proof and an intelligible argument. His example was a future proof so extensive that no person could survey it as a whole. A computer might certify its validity while human beings remained unable to grasp what made it work. The distinction gave me a better account of the controversy, but it also provoked an objection: why should the limits of human understanding become the limits of mathematics? (Luo, n.d.) At first, this explanation seemed to locate the missing issue: a successful derivation might leave the human purpose of doing mathematics unfulfilled. But it also seemed to move too quickly from a claim about what mathematicians value to a claim about what should count as mathematics. I could accept the first claim and still resist the second. That resistance, more than a simple preference for machines over people, drove the questions that followed.
That objection became the thread I kept pulling. It led from proof to intuition, from intuition to beauty, from beauty to Plato, and eventually to questions about institutions, authority and the distribution of intellectual work. At several points, the AI helping me develop the inquiry offered a useful distinction, and I responded with another version of “yes, but.” Human understanding matters to us, I kept insisting. Does it follow that mathematics itself must be organized around what we can understand? I was particularly struck by the apparent return of an ancient philosophical dispute in response to a technological development. Why should a faster way of finding proofs make us reconsider what mathematics is? My question gradually shifted from whether AI was good for an existing activity to whether we had understood the boundaries of that activity in the first place.
I still think the objection survives. I have become more careful, however, about what the recent evidence establishes. The events discussed here, considered through 1 November 2026, show a rapidly changing relationship between mathematical discovery and human intellectual labour. They do not establish that AI has reached a realm permanently inaccessible to human thought. Keeping those claims apart has become central to what I now want to understand.
The question hidden inside the word mathematics
The first difficulty is that “mathematics” can name several things at once. It can refer to structures and their properties, to systems of definitions and deductions, to the activity of investigating those structures, or to a community that decides which investigations deserve attention. These meanings overlap, but a claim about one does not automatically settle a question about another.
When I say that an undiscovered mathematical property might hold independently of our understanding, I am making a claim about what there is to investigate. When a mathematician says that the purpose of mathematics is to deepen understanding, they may be describing a human practice and its aims. Those positions can coexist. A medical discovery can matter before anyone understands its mechanism, while explaining that mechanism remains an important purpose of medicine. The analogy does not resolve mathematical ontology, but it prevents a disagreement about purposes from masquerading as a disagreement about validity. This explains why an appeal to the importance of understanding did not fully answer my objection. I was asking whether our inability to grasp a structure could disqualify it; the appeal explained why people would want to grasp it. Both questions are legitimate. Recognizing that the conversation had moved between them helped me preserve the objection without dismissing the human concern.
The comparison with Go in Luo’s answer helped expose the difference. A surprising move can win under agreed rules even when observers cannot explain why it is strong. That makes it a useful analogy for separating successful performance from an account of the strategy. But a winning condition does not tell us what research questions to pursue, what connections deserve attention, or what a community should learn. Autonomy in searching for a result and independence from the rules or purposes of the activity are separate matters. The analogy made mechanical assessment easier to imagine; it could not supply a complete account of mathematical value.
This was also where my initial impression that mathematics had little to do with philosophy needed revision. Questions about mathematical existence, the warrant provided by a proof, and the relation between symbols and meaning were already philosophical questions. AI makes their consequences harder to avoid in ordinary research. William Thurston’s account of mathematical progress, written in 1994, already treats communication and the development of understanding as central to the discipline. It provides a much richer position than the slogan that mathematicians simply want more theorems (Thurston, 1994). AI did not introduce philosophy into a previously philosophy-free subject. My interpretation is that it made some familiar connections less secure: the person who discovers, the community that verifies, and the readers who acquire understanding need no longer move at comparable speeds. Assumptions about their relationship consequently become matters of explicit debate.
The distinction I found most useful in the AI-assisted discussion was between discovery, verification, explanation and significance. Finding a proof answers a different question from checking it. Checking it need not explain why its strategy was promising. Understanding the strategy does not automatically reveal where else it will work. And none of these achievements, by itself, establishes that the theorem deserves the attention of a research community.
Luo had already mentioned the four-colour theorem, and returning to that example gives the discussion a longer history. In 1979, Thomas Tymoczko argued that the computer-assisted proof forced a reconsideration of what a proof could be. His concern was surveyability: whether a rational agent could inspect the reasoning that justified the conclusion. He interpreted the reliance on computer execution as introducing an empirical element into mathematical warrant. That was a philosophical argument about the proof’s status, not a discovery of an error in its mathematics (Tymoczko, 1979). The historical point matters to my question. Generative AI has intensified a separation that earlier computational proofs had already made difficult to ignore.
These distinctions also clarify the role of formal verification. A proof assistant checks that a precisely expressed conclusion follows under specified assumptions and rules. There remains a question about whether the formal statement faithfully expresses the mathematical claim people intended to make. A changed quantifier or an unexpectedly strong hypothesis can matter enormously. Thomas Hales’s recent discussion of Lean is valuable because it examines the actual architecture of trust and the conditions on which reliable checking depends (Hales, 2026).
The formal relationship can be expressed compactly. Let \(\Gamma\) denote a collection of assumptions and \(\varphi\) a precisely formulated statement. In a sound proof system, the following implication holds:
\[
\Gamma\vdash\varphi
\quad\Longrightarrow\quad
\Gamma\models\varphi.
\]
The expression on the left says that \(\varphi\) has a derivation from \(\Gamma\); the expression on the right says that \(\varphi\) holds in every interpretation satisfying those assumptions. Soundness connects these two kinds of claim. It does not independently certify the assumptions or establish that the formal statement captures the problem someone intended to solve. This is the point at which a compact logical guarantee still requires care about meaning.
A change in quantifier order makes that concern concrete. Consider these two statements about real numbers:
\[
\begin{aligned}
&\forall x\in\mathbb R\;\exists y\in\mathbb R:\;y>x,\\
&\exists y\in\mathbb R\;\forall x\in\mathbb R:\;y>x.
\end{aligned}
\]
The first says that every real number has a larger real number; choosing \(y=x+1\) proves it. The second says that one real number is larger than every real number, which fails as soon as we set \(x=y\). The symbols differ only in the order of their quantifiers, but the claims differ decisively. Checking a proof of the first would give no warrant for announcing the second. Auditing what was formalized and auditing the derivation are therefore distinct responsibilities.
A recent philosophical response makes the disagreement more precise. Eamon Duede and Kevin Davey argue that an opaque system can provide a proof whose checking is sufficiently transparent to yield a priori mathematical knowledge, even when a human cannot survey the entire proof. Their claim depends on the character of the checker and its relation to accepted reasoning; it is not an invitation to believe an unaccompanied machine assertion (Duede and Davey, 2025). I take this as a useful counterweight to treating opacity as one undifferentiated obstacle. The opacity of discovery, the accessibility of verification and the absence of an explanatory account can come apart.
Once that correspondence has been established and the proof checked, however, ignorance of how the proof was discovered does not invalidate the deduction. Otherwise, we would make the discoverer’s psychology part of the theorem’s justification. I can learn from an argument whose invention I cannot reconstruct. I can also have good grounds for accepting a result without possessing the expertise needed to explain its deepest consequences. These are different kinds of intellectual access, and the conversation became more productive when we stopped compressing them into the single word “understanding.”
A proof we could not find is not necessarily a proof we cannot understand
The distinction between access and existence sounded convincing in the abstract. I then asked the AI to be exact about the limitation under discussion. Was it a limit of memory, of available techniques, of a particular researcher’s knowledge, or of human thought as such? I supplied the local-smoothing announcement together with the detailed commentary surrounding it. This changed the task: a general philosophical reassurance now had to survive contact with a specific mathematical case.
OpenAI’s 26 October release reported a proof of the local-smoothing conjecture for the Euclidean wave equation in every spatial dimension at least two, with consequences for other major problems in harmonic analysis. According to the announcement, the mathematical output was obtained on 18 October and formalized in Lean the following day. I brought this example into the discussion because it seemed to embody the possibility that AI had moved beyond the limits of human mathematics (OpenAI, 2026b).
The surrounding commentary encouraged that interpretation. Decades of human effort were compared with a few days of machine work. Some responses treated an earlier breakthrough as retrospectively diminished by a later, more general result. Yet elapsed time is a poor measure of independence: a system may draw on a vast accumulated literature, computational infrastructure and previous mathematical labour. Nor does a later theorem erase the knowledge created along the way. The rhetoric of a race between species can conceal the intellectual inheritance on which the race depends.
More importantly, the supplied account describes a short central argument within a longer manuscript, built around a new auxiliary partial differential equation. That is not the same scenario as a billion-line proof that no human can survey. In the manuscript, an energy correction cancels a troublesome determinant term. Suppressing the analytic definitions, the cancellation can be represented schematically as follows:
\[
\begin{aligned}
\Delta X &= B-P-D,\\
\Delta E &= D,\\
\Delta(X+E)+P &= B,\qquad P\geq 0.
\end{aligned}
\]
Here \(X\) is the initial quantity, \(E\) a correction, \(D\) the term being cancelled, \(B\) a boundary contribution, and \(P\) a nonnegative term. This is a sketch of one mechanism, not a substitute for the proof. The auxiliary objects must exist, boundary terms must be controlled, and the corrected quantity must retain useful estimates. The mathematical achievement lies in constructing a setting where this cancellation has the required consequences (OpenAI, 2026a).
That small piece of structure changed how I read the example. It gives me something conceptually recognizable: introduce an auxiliary construction, modify a quantity, cancel an obstruction, recover an estimate. Recognizing that architecture does not mean I can certify the argument. I have not independently audited the complete analysis or rebuilt the formalization. It does mean that the philosophical inference needs to be narrower. A method can be very difficult to invent and still become intelligible after someone—or something—has found it.
The accompanying commentary also stressed the unfamiliar combination of tools. This suggested another interpretation of the human difficulty: a research community may have developed powerful techniques along one route while a productive connection lies across disciplinary boundaries. Such a connection can be hard to find without being beyond human thought. Equally, describing its components as already known would not explain away the achievement of assembling them. Once a proof is available, its economy can make the original search look deceptively easy. The claims that AI found this route, that people had not found it, and that only AI could ever have found it require progressively stronger evidence.
There are several possible limits here. An individual may lack the relevant training. A community may not yet possess the right conceptual language. A search may demand more time or memory than its researchers can supply. An argument may be too large for direct inspection but admit a useful explanation at another level. Finally, there is the much stronger possibility that no human-accessible explanation exists. Evidence for the earlier possibilities does not establish the last one. The pronoun “we” also needs care. One person, a trained specialist, a research community and a community equipped with new notation and computational tools have different capacities. A limit established for one of these is not automatically a limit of the others. This makes collective learning part of the question itself, not an incidental remedy applied after a fixed human boundary has been reached.
The original Zhihu answer had also imagined a more radical case in which even the definitions and theorem statement exceeded human comprehension. The local-smoothing example does not establish that scenario. It concerns a question humans had already formulated and recognized as important. An unfamiliar route to a familiar destination and an unfamiliar mathematical world are different possibilities. I had been drawn to both, but this example could support only a more limited conclusion.
I therefore no longer regard this case as a demonstration of permanent human incomprehensibility. It is a powerful example of the gap between finding an approach and understanding an approach once it has been supplied. That gap matters enormously, but calling it an absolute epistemological wall would settle the philosophical question before the investigation had begun. This correction does not prove that every valid argument will eventually become intelligible to us. That would reverse the overconfidence without removing it. What survives is the possibility of mathematics beyond our present reach; what must be withheld is the claim that this particular result demonstrates an unchangeable boundary.
Intuition may arrive after discovery
My initial question assumed that human understanding was a relatively fixed capacity against which new mathematics could be measured. The literature introduced another possibility: the discovery may change the capacity doing the measuring. I had also asked for recent work by people close to mathematical research, ideally able to engage its philosophical questions. A general account of Plato or formalism could clarify the vocabulary, but I wanted to know how researchers were interpreting the actual changes in their work. This request led the discussion toward the papers by Michael Friedman and Kati Kish Bar-On.
Michael Friedman and Kati Kish Bar-On’s discussion of mathematical intuition is helpful here. They examine how AI can alter the relationship between producing mathematical material and interpreting it. Their cases include situations in which researchers develop intuition retrospectively, after a system has generated an unexpected result or object. The implication I take from their work is that intuition has a history. What feels natural to a mathematician can depend on the representations, examples and practices through which that person has learned to think (Friedman and Kish Bar-On, 2026a).
This complicates the contrast between human insight and machine output. A strange construction may initially look like an accident. After sustained investigation, it may become an example of a general phenomenon, and eventually something that students learn to recognize. The point is not that every opaque result will yield to explanation. It is that present opacity is a condition of our relationship to a result, not automatically a permanent property of the result.
Jeremy Avigad’s earlier Varieties of Mathematical Understanding helps prevent the word “understanding” from becoming an unexplained badge of approval. Through examples from discrete geometry, he questions whether familiar standards of conceptual depth adequately accommodate computational work that supplies new representations, methods and capacities for reasoning (Avigad, 2022). I would make the practical question explicit: can someone recognize when a result applies, explain why a hypothesis matters, identify a failure when that hypothesis is removed, or adapt the method to another problem? These are ways of investigating understanding without assuming that it consists solely in a private feeling of insight. They also leave room for several kinds and degrees of understanding.
An elementary comparison makes the difference between obtaining an answer and acquiring a reusable method concrete. Calculating separate totals for \(1+2+\cdots+n\) gives correct answers for the values tried. Pairing the same sum with its reversed order reveals a relation valid for every positive integer \(n\):
\[
\begin{aligned}
S_n &=\sum_{k=1}^{n}k,\\
2S_n &=\sum_{k=1}^{n}\bigl(k+(n+1-k)\bigr)=n(n+1),\\
S_n &=\frac{n(n+1)}{2}.
\end{aligned}
\]
The pairing explains why the quadratic expression appears: there are \(n\) pairs, each contributing \(n+1\), and the construction counts the original sum twice. It also suggests how to handle other arithmetic progressions. This small example gives substance to the desire for understanding. An investigator acquires a way to organize further reasoning, alongside confidence in the answer. Whether a complicated machine-generated proof admits an equally useful reorganization remains a question to investigate in each case.
A particularly useful example is Bruhat intervals that are large hypercubes. Ellenberg and his collaborators describe how permutations suggested by AlphaEvolve led them to an interpretable pattern and a general theorem. In discussing their methodology, they also contrast this experience with AI-generated improvements in cap-set constructions for which satisfying explanations may remain unavailable. The same broad approach can produce material that becomes conceptually illuminating or material whose success remains difficult to explain (Ellenberg et al., 2026). I kept returning to this contrast because it resisted both easy conclusions. An opaque improvement does not guarantee a hidden explanation waiting to be extracted. An interpretable construction prevents us from treating machine discovery and human insight as mutually exclusive. What mattered was the possibility that the same methodology could lead in either direction.
Another research account, concerning the Grothendieck constant, makes the interaction less tidy still. A sustained AI search for improved upper bounds encountered a plateau. Human collaborators helped redirect the investigation toward what the failures might reveal about limitations of the approach. The system then contributed substantial mathematical work to the redirected programme. The authors describe both strong technical performance and weaknesses in maintaining research judgement over an extended investigation (Li et al., 2026).
I find this kind of account more informative than either a celebration of autonomous genius or a reassurance that humans will always supply the important ideas. It records where judgement was needed in a particular collaboration. It does not prove that the same division of labour will persist. A weakness observed in one system is evidence about that system and that research process; turning it into a permanent boundary around human creativity would repeat the mistake I was trying to avoid.
The distinction also reaches back into my own inquiry. AI helped formulate connections, organize sources and sharpen alternatives. My repeated contribution was to resist the point at which a defence of human understanding quietly became a restriction on what mathematics was permitted to contain. The resulting argument belongs to that interaction. Its fluency cannot serve as evidence for its truth; the sources, distinctions and unresolved objections still have to carry the weight. The exchange was consequential precisely where a formulation returned as a new question. Once the AI had distinguished a limitation in access from a limitation in mathematical reality, I asked what kind of limitation an actual breakthrough revealed. My supplied example then required that distinction to become more precise. That sequence gave my questioning a role beyond accepting or rejecting a finished answer.
What beauty can tell us, and what it cannot decide
The discussion of beauty initially strengthened my suspicion that mathematics might be organized around human limitations. Perhaps an elegant proof is one that fits into our memory. Perhaps symmetry appeals to us because it makes a complicated object easier to handle. If another intelligence could work productively with structures we find unwieldy, why should our aesthetic preferences determine their mathematical worth?
There is a real question here, but my first formulation was too quick. When I read Rita Ahmadi’s essay, I objected that mathematicians praised beauty without even defining it. On closer attention, she does offer a definition, centred on simplicity, surprise and a sense of vitality. She also reports disagreements about what simplicity means: a short argument, few prerequisites, an accessible statement or a clear organizing idea. The stronger criticism is therefore not that no definition exists. It is that the proposed criteria do not settle every case, and their relationship to mathematical value remains contestable (Ahmadi, 2026). The correction leaves my original concern intact in a stronger form. Even a thoughtful account of beauty must still explain why its criteria should govern mathematical worth, and how far those criteria depend on the audience. I had challenged an absence of definition; the more productive question concerned the authority and scope of the definitions available.
There is a further complication in my suggestion that elegance accommodates limited memory. A short argument can conceal an enormous library of prior work; an elementary argument may require many more steps while relying on fewer concepts. Brevity therefore depends partly on the language and background knowledge in which a proof is expressed. This gives substance to Ahmadi’s different senses of simplicity. It also suggests that new mathematical languages could change what either people or machines find economical. Counting lines or noticing a pleasing pattern cannot, by itself, tell us whether the economy belongs to the representation, the underlying structure, or both.
That correction matters because disagreement about a concept does not make it empty. Mathematicians can recognize important differences between two proofs without possessing a universal aesthetic measuring device. A proof that reveals a reusable mechanism may be more valuable for further research than an exhaustive verification. A construction that joins previously separate questions can change what investigators are able to ask. These are intelligible reasons for admiration, even when people disagree about the word “beautiful.”
My suggestion about memory also needs qualification. Symmetry is a mathematically specifiable property. Particular human beings may find a symmetry beautiful, useful, irrelevant or misleading, but their response does not create the invariant relationships involved. Likewise, a reusable abstraction can reduce repeated work for any investigator facing finite resources. It is plausible that some preferences we experience aesthetically track features valuable to more than one kind of intelligence. It would be equally premature to declare them universal standards or mere biological conveniences. For a simple example, rotating a square through a right angle preserves its geometric relations, independently of whether an observer admires the result. The preference for studying such invariance is one question; the invariance itself is another. My original suspicion concerned the selection of mathematical objects, and it should not be allowed to erase the properties of the objects selected.
For a square centred at the origin, this invariance can be written explicitly. The matrix \(R\) represents a quarter-turn, \(I\) is the identity matrix, and \(\|\mathbf u-\mathbf v\|_2\) denotes the usual distance between two points in the plane:
\[
\begin{aligned}
R&=\begin{pmatrix}0&-1\\1&0\end{pmatrix},
\qquad R^{\mathsf T}R=I,\qquad R^4=I,\\
\|R\mathbf u-R\mathbf v\|_2&=\|\mathbf u-\mathbf v\|_2.
\end{aligned}
\]
The rotation permutes the square’s vertices while preserving distances, and four applications return every point to its starting position. These are checkable relationships. An observer’s admiration, indifference or preference for another class of objects does not alter them. What remains open is how far an intelligence’s preference for such relationships guides its selection of worthwhile mathematics.
Three questions became distinct for me: what makes a mathematical construction effective, what makes it beautiful to an audience, and what its producer experiences while creating it. An AI-generated argument might satisfy human criteria of elegance whether or not the system experiences anything resembling aesthetic pleasure. Conversely, a construction may support important mathematics while leaving its human readers unmoved. The emotional experience of the maker is not part of the logical warrant for the result. Ahmadi’s closing uncertainty about creativity and emotional experience made this separation especially useful. A question about whether a machine can feel the pleasure of discovery cannot, on its own, decide whether people can find its output beautiful. Nor would our pleasure establish the result’s validity. The maker’s experience, the reader’s response and the argument’s justification must each be examined on their own terms.
This leaves room for a more demanding view of beauty. We can value it as a way of orienting attention without treating it as a guarantee of truth or a veto over unfamiliar mathematics. We can also ask whether new discoveries will educate our taste. If AI exposes patterns we initially find ugly because we lack the right representation, our aesthetic judgement may eventually change. That is a possibility worth investigating, not a promise that every difficult object conceals a pleasing explanation.
Could there be mathematics beyond the human measure?
The idea that most interested me was the possibility that human mathematics occupies a selective region of a larger landscape. We explore what our perceptual habits, languages, tools, institutions and historical encounters make accessible. Another kind of investigator might travel differently.
Barkeshli, Douglas and Freedman give this thought a research programme in Artificial Intelligence and the Structure of Mathematics. Their proposed computational metamathematics studies relationships between a broader space of formal mathematics and the portions developed by humans. They ask whether features of human mathematics reflect intrinsic organization, historical contingency, cognitive constraints or some combination. Their framework offers ways to investigate those questions; it does not already demonstrate the existence of a comprehensively mapped, mind-independent mathematical universe (Barkeshli, Douglas and Freedman, 2026). The proposal changed the next question I wanted to ask. My earlier image had been a wall at the edge of human knowledge. Here was a way to investigate how our routes through mathematics are selected. The issue became less a single boundary to announce than a pattern of access, omission and possible alternatives to study.
What became newly thinkable for me was a change in the direction of inquiry. Instead of asking only whether AI can succeed at questions we have selected, we could ask what it selects when given greater freedom to define objects, formulate questions and organize a research programme. Would independently developed systems converge on familiar structures? Would they find different abstractions that nevertheless explain our results? Would some of their most productive concepts remain cumbersome to translate into our languages?
These would be substantive discoveries about mathematical practice. They would still require interpretation. Convergence might reflect shared mathematical constraints, but it could also reflect common training material, objectives or formal libraries. Divergence might reveal a productive alternative, or simply an arbitrary response to an artificial reward. Present systems are deeply connected to human mathematics. Describing them as an independent alien civilization would conceal that dependence.
My excitement about a potentially different mathematical landscape therefore needs a methodological condition. To learn something about the influence of human cognition, we would have to examine which human choices remain built into the experiment: the formal language, available library, search budget and measure of success. A system rewarded for solving familiar conjectures may become exceptionally good at extending familiar mathematics. That achievement would not yet answer what it might investigate under different objectives. Computational metamathematics is interesting to me because it could make these choices objects of study, provided we do not mistake a particular search environment for mathematics as a whole.
This is where Plato entered my questions. A structure that resists our expectations can feel like evidence of something waiting to be discovered. Yet successful AI mathematics would not by itself decide between Platonism, structuralism and more formalist interpretations. These positions can explain many of the same mathematical practices while disagreeing about what their success commits us to. A proof assistant’s acceptance of a derivation does not include an additional certificate establishing the metaphysical status of its objects.
A related disagreement emerged over the word “meaningful.” In the discussion, the AI challenged the strong interpretation that a generated object would lack mathematical status until a human made sense of it. I found that correction useful, but wanted to know what it left of the arguments for human interpretation. Making a result intelligible within a community and bringing its properties into existence are different claims. The former can be defended without assuming the latter.
A more modest example helps. Suppose a terminating program, under specified semantics, generates a definite finite graph. Whether that graph contains a particular cycle does not ordinarily depend on whether a human has recognized the cycle. The object can constrain our answers before we understand its organization. That observation supports the practical distinction between determination and recognition. It does not require a supernatural realm, and it does not settle every philosophical question about mathematical existence. Its importance for my argument is limited but precise: recognition can reveal a constraint that was already fixed by the construction. Whether that constraint deserves sustained investigation introduces further questions about usefulness, connections and possible understanding. I should not collapse those questions into the claim that every determined property is equally valuable.
A triangle gives a concrete instance of such a property. Number the vertices of a finite simple undirected graph from \(1\) to \(n\), and form its adjacency matrix \(A\): the entry \(A_{ij}\) is \(1\) when vertices \(i\) and \(j\) are joined and \(0\) otherwise, with zero entries on the diagonal. If \(t(G)\) is the number of triangles, then:
\[
t(G)=\frac{\operatorname{tr}(A^3)}{6}
=\frac{1}{6}\sum_{i,j,k=1}^{n}A_{ij}A_{jk}A_{ki}.
\]
The trace is the sum of a matrix’s diagonal entries. Here it counts closed walks of three edges. Each triangle contributes six: three choices of starting vertex and two directions of travel. A sufficiently large graph can therefore be tested without a reader recognizing a triangle in a drawing. The calculation settles a definite property of the constructed object. Explaining why a family of such graphs produces many triangles, or why that feature matters elsewhere, introduces further questions. This is a small, explicit example of how determination, verification and significance can come apart.
The sentence from the AI-assisted discussion that I kept returning to was this: a limitation in our access does not entail a limitation in what there is to access. Its force is negative. Our failure to understand something does not establish its impossibility or insignificance. The sentence does not license the reverse inference that every imagined structure exists, that every opaque output is profound, or that an incomprehensible result must be correct.
I also wondered whether AI doing mathematics could be described as mathematics encountering itself. I still find the image suggestive, provided it remains an image. A system describable mathematically is producing further mathematical representations. Calling that “self-encounter” does not establish awareness, privileged access to truth or a new metaphysical subject. “Silicon mathematics” and “carbon mathematics” are similarly provocative descriptions of different investigative practices. They should not imply that a valid consequence of the same assumptions becomes true for one substrate and false for another. Different agents could prefer different axioms, representations or problems, so their mathematical activities need not coincide. The claim about shared consequences applies when the assumptions and meanings really are shared. Likewise, talk of an AI’s different “beauty” could refer to the structures its search tends to favour; that observable preference would not establish an inner aesthetic experience. These qualifications preserve the possibility of unfamiliar mathematics without turning a metaphor into evidence about a machine’s mind.
Further reading also brought a direct challenge to my position. In his October essay, Avigad argues that mathematics serves our reasoning and deliberation, and that developments matter to us through historically and culturally situated values. Mathematical activity pursued only for the interests of AI agents would not, on that account, fulfil the human purpose of the discipline (Avigad, 2026b). I understand the force of this claim as a defence of human agency. My remaining objection concerns its scope. A decision about what human institutions should support cannot establish that other productive mathematical practices lack value for every possible investigator. Nor can present unfamiliarity tell us which of those practices might eventually become consequential for us.
My own movement toward theology began with the thought that something might be correct, intelligible to another kind of intelligence, and still exceed us. I wondered whether this was becoming a claim about a higher order of reality. Yet “beyond my understanding” describes a relation to a knower; “divine” makes a much stronger claim about the status or source of what exceeds us. The transition between them requires an argument. The theological possibility therefore remains a further question; the mathematical evidence alone does not establish it. Discovering that human thought is limited would be compatible with many theological views, but it would not demonstrate divine intelligence or purpose. Acknowledging what exceeds us can be intellectually and existentially significant without deciding what, if anything, makes that excess sacred. I do not want to replace an unjustified confidence in human centrality with an equally unjustified mystification of the machine.
Objectivity does not remove the question of power
As the discussion moved toward the mathematician’s changing position, I began to see why a controversy about proof could also become a controversy about authority. If producing a difficult proof has been a major source of professional recognition, a technology that changes who can produce proofs will disturb the institutions built around that achievement. That does not make the mathematics subjective. It makes the production and organization of mathematical knowledge a social activity. The suggestion that mathematicians might lose a privileged position caught my attention because mathematics had seemed to me an especially secure domain of intellectual authority. If even this discipline could not escape questions of status and recognition, perhaps its apparent distance from the social world had been misleading. That was a reason to investigate its institutions, however, and not evidence about any individual mathematician’s motives.
Michael Friedman’s account of mathematical anxiety examines opacity and the inversion of familiar roles: a mathematician who expects to create an argument may instead be asked to interpret or validate machine output. I found this useful because it names a possible disturbance in intellectual identity. Friedman presents it as an interpretive framework, alongside other explanations of concern. It is not an empirical diagnosis of every mathematician who objects to AI (Friedman, 2026).
That qualification changed my own reaction. It would be too easy to explain the entire controversy as injured privilege. Some criticisms concern defective arguments, attribution, access or the direction of research. Their merits must be examined independently of speculation about the critic’s emotions. I can ask how authority is changing without pretending to know why a particular person feels threatened.
Friedman and Kish Bar-On’s work on the redistribution of epistemic labour adds a more institutional perspective. It directs attention to how resources, authority and recognition are arranged around AI-based research. Mathematics already depended on collective labour and unequal access before these systems arrived. The question is how the new arrangements intensify, modify or potentially improve those relationships (Friedman and Kish Bar-On, 2026b).
This also made me reconsider the original Zhihu answer’s self-mocking picture of people who mainly consume and interpret other people’s mathematics. If that becomes a larger part of professional work, does it necessarily amount to demotion? The Bruhat example suggests why the answer cannot be automatic: interpretation can lead to generalization and further discovery. The value of that work must be assessed through what it contributes. Describing it as secondary because it comes later would confuse the order of an investigation with the importance of its parts.
The October release debates make the issue concrete. OpenAI described its outputs as raw research material and experimented with different arrangements for expert collaboration and public release. It also acknowledged that selecting initial collaborators can create asymmetries. The Advisory Group on Mathematics and Artificial Intelligence argued that designated intermediaries can affect community agency even when the underlying material is public, and called for immediate release of the announced quantum-field-theory outputs (OpenAI, 2026b); (AGMAI, 2026).
The disagreement is consequential even if everyone involved welcomes mathematical progress. Who receives access to powerful systems? Who chooses the questions those systems pursue? Who gets the first opportunity to interpret a result? Who receives credit for turning a difficult output into a usable theory? A laboratory’s decision to forgo academic authorship does not automatically remove its influence over the research agenda. Equally, putting a manuscript online does not give every researcher comparable access to the system that produced it. This also changes the meaning of a loss of human privilege. The declining importance of one person’s ability to produce proofs could coexist with increased power for the people and organizations controlling the strongest systems. That is a possible institutional outcome, not an inevitable one. It is why I now distinguish the displacement of a familiar mathematical role from the distribution of power around the role that replaces it. Making discovery less dependent on an individual genius does not, by itself, make participation more equal.
This is why the truth of a theorem cannot settle the organization of the field. A proof can be valid while the arrangements surrounding it remain open to criticism. Conversely, an admirable release process cannot repair an invalid proof. Both forms of judgement are necessary, and neither should be used to silence the other.
What remains open after the theorem is proved
I eventually returned to a question I had asked more than once: are these debates still open, and what is mathematics actually doing next? By then, answering only that the future was uncertain would have been inadequate. Some distinctions had become clearer even while the forecasts remained unsettled. An unfamiliar proof is not thereby invalid; a checked proof is not thereby explanatory; a valuable explanation need not settle who should control access to the research. The remaining questions had to be separated before they could be pursued. In this sense, “crisis” names unsettled relationships among proof production, understanding and professional judgement. It need not suggest that mathematical inference has ceased to work.
By the beginning of November, the response had already moved beyond general declarations of enthusiasm or alarm. A Harvard CMSA summit brought together mathematicians from academia, government and industry and published recommendations concerning research evaluation, formalization, tools and collaboration with AI laboratories. Its organizers explicitly urged changes in departmental practices, with particular concern for students and early-career researchers (Freed et al., 2026).
Frank Calegari’s 1 November essay similarly combines recognition of substantial AI contributions with criticism of presentation and attribution, then turns toward hiring, publishing and training. These interventions do not amount to a settled consensus. They do show that the field’s immediate questions concern the design of mathematical work as much as the capabilities of models (Calegari, 2026).
Avigad offers another practical direction in What is mathematics now, and what should it be?: broaden the activity described as AI for mathematics. He includes formal libraries, symbolic reasoning, data exploration, new interfaces and the development of mathematical tools, alongside neural theorem proving. He also argues for recognizing such contributions in training and professional evaluation (Avigad, 2026a). This responds to a concern that had been implicit in my questions. Mathematicians need not be positioned only as recipients of completed proofs. They can help determine what systems are built, what kinds of inquiry those systems enable, and how the results become available to others.
I now see three different kinds of open question. Some are empirical. Can systems reliably invent useful definitions and sustain research programmes? Can they produce explanations that help people solve unfamiliar problems, and how would we distinguish that achievement from an explanation that only sounds satisfying? When a search produces an unexpected object, can its significance be assessed without quietly importing all the standards from the human tradition we hoped to investigate? These questions call for documented research processes, reproducible evidence and comparisons that distinguish assistance from autonomous performance.
Other questions concern what institutions should value. How should mathematical credit be shared among discovery, formal verification, exposition, tool-building and the creation of new questions? What should students learn when solutions and explanations become much easier to obtain? How can researchers retain the ability to choose their own problems when the strongest tools are unevenly distributed? More output does not automatically produce more opportunity, and the availability of an explanation does not mean that a learner has acquired the ability to reason with it.
Still other questions are philosophical. What makes a result mathematically significant beyond the attention it currently receives? How much of our sense of depth comes from the structure investigated, and how much from the difficulties of our route toward it? Can there be kinds of mathematical organization that are productive for another intelligence while remaining inaccessible to us? These questions may become better informed by AI, but no single benchmark or proof announcement can settle them.
One response I now distrust is the attempt to assign humans a permanently protected final task. We might say that machines will prove theorems while humans will always choose the questions, explain the ideas or judge beauty. Those may describe useful arrangements today. They are not established laws of intelligence. If AI becomes better at explanation or research judgement, the value of human participation will need a justification more durable than the prediction that machines cannot perform it.
One response in the material I supplied compared intellectual competition with sport after the mechanization of physical work. The analogy makes a legitimate point: an activity can retain human value even when a machine outperforms us. But it does not settle the future of research. Mathematics contributes to science, engineering and shared reasoning, as well as to the lives of the people who practise it. I would therefore separate the case for continuing to learn and do mathematics from the question of how professional research should organize its contribution. The first does not depend on winning a contest with AI; the second still requires evidence about what different arrangements make possible.
The AI-assisted discussion eventually offered a formulation I could work with: human understanding should remain a major purpose of mathematical research without becoming a universal admission requirement for mathematical validity. A result need not wait for an intuitively satisfying explanation before it can be used, provided its statement and justification are sound. At the same time, there are strong reasons to support the slow work of explanation, education and conceptual development. Those reasons concern the kind of intellectual life we want to sustain, as well as the further discoveries such work makes possible. I found the formulation useful because it gave human understanding a defensible place without making human cognitive limits into laws of mathematical existence. Its justification remains a judgement about the purposes of our institutions; further AI progress may change how we pursue those purposes.
This position leaves a tension in place. If I accept that mathematics can exceed our present understanding, I cannot demand that every valuable discovery eventually become comfortable for us. If I value understanding, I also cannot treat a growing archive of certified statements as the complete fulfilment of mathematical inquiry. I have to allow both the possibility of irreducible opacity and the possibility that what appears opaque today will educate a future reader.
The question I began with was whether AI proving mathematics should count as good news. The route to this point was not a conversion from enthusiasm into scepticism, or from confidence in people into confidence in machines. Each answer changed what I needed to ask next. I now want to ask what we are prepared to do with that good news, and what standards will help us distinguish genuine enlargement from an accumulation we cannot use. The most interesting possibility is that AI changes both sides of the encounter: the mathematical territory available to us and the forms of understanding through which we enter it. The limits may move, and we still have to learn how to recognize which limits are moving.
References
Advisory Group on Mathematics and Artificial Intelligence (AGMAI). 2026. “Disadvantages of Designating Mathematicians for AI Output Releases” and “Recommendation for Immediate Release of Yang–Mills AI Output.” Statements, 25 and 26 October. AGMAI website.
Ahmadi, Rita. 2026. “The Eye of the Mathematician.” Aeon, 9 March. Read the essay.
Avigad, Jeremy. 2022. “Varieties of Mathematical Understanding.” Bulletin of the American Mathematical Society 59: 99–117. https://doi.org/10.1090/bull/1726; author’s deposited version.
Avigad, Jeremy. 2026a. What Is Mathematics Now, and What Should It Be? Preprint, arXiv:2608.23218, 24 August. Read the preprint.
Avigad, Jeremy. 2026b. “The Future of Mathematics.” Guest essay on Terence Tao’s What’s New, 5 October. Read the essay.
Barkeshli, Maissam, Michael R. Douglas and Michael H. Freedman. 2026. Artificial Intelligence and the Structure of Mathematics. Preprint, arXiv:2604.06107. Read the preprint.
Calegari, Frank. 2026. “Mathematics Has Changed. Let’s Act Like It.” Guest essay on Terence Tao’s What’s New, 1 November. Read the essay.
Duede, Eamon, and Kevin Davey. 2025. “A Priori Knowledge in an Era of Computational Opacity: The Role of Artificial Intelligence in Mathematical Discovery.” Philosophy of Science 92 (5): 1394–1404. https://doi.org/10.1017/psa.2025.10160.
Ellenberg, Jordan, Nicolas Libedinsky, David Plaza, José Simental and Geordie Williamson. 2026. Bruhat Intervals That Are Large Hypercubes. Preprint, arXiv:2601.01235. Read the preprint.
Freed, Dan, Larry Guth, Bryna Kra, Emily Riehl and Mohammed Abouzaid, organizers. 2026. “Recommendations from the Harvard CMSA Summit on Math and AI.” Proofs and Prompts, 30 October. Read the announcement and linked report.
Friedman, Michael. 2026. “Mathematical Anxiety in the Age of AI: Opacity, Role Inversion, and the Changing Place of the Mathematician.” Computers in Human Behavior: Artificial Humans 9: 100386. https://doi.org/10.1016/j.chbah.2026.100386.
Friedman, Michael, and Kati Kish Bar-On. 2026a. “Rethinking Mathematical Intuition in the Age of AI.” The Mathematical Intelligencer, published online 26 August. https://doi.org/10.1007/s00283-026-10561-y.
Friedman, Michael, and Kati Kish Bar-On. 2026b. “Big AI-Based Mathematics and the Redistribution of Epistemic Labor.” Social Studies of Science, published online 7 October. https://doi.org/10.1177/03063127261482050.
Hales, Thomas. 2026. “What Mathematicians Should Know About the Lean Theorem Prover: Questions of Reliability and AI.” Guest essay on Terence Tao’s What’s New, 9 October. Read the essay.
Li, Alan, Rahul Saha, Anton Xue, Swarat Chaudhuri, Adam Klivans, Pravesh K. Kothari and Raghu Meka. 2026. Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human–AI Mathematical Collaboration. Preprint, arXiv:2608.11195, version 3. Read the preprint.
Luo Xincheng (罗心澄). n.d. Answer to “OpenAI利用人工智能解决数学问题不是一件好事吗？为什么会引起数学界的争议？” Zhihu. Text supplied in the conversation. Read the answer.
OpenAI. 2026a. Local Smoothing for the Euclidean Wave Equation. AI-generated manuscript, 25 October. Manuscript; formalization scope documentation.
OpenAI. 2026b. “Working with Academic Communities to Build Scientific Understanding.” Research announcement, 26 October. Read the announcement.
Thurston, William P. 1994. “On Proof and Progress in Mathematics.” Bulletin of the American Mathematical Society 30: 161–177. Author’s preprint.
Tymoczko, Thomas. 1979. “The Four-Color Problem and Its Philosophical Significance.” The Journal of Philosophy 76 (2): 57–83. Read the article.