Can AI truly prove anything?

Stepan Nesterov, PhD student at Stanford University

About a hundred years ago, David Hilbert gave a rigorous definition of a mathematical proof:

Definition. A mathematical proof is a sequence of formal statements $A_1, \ldots, A_n$ such that every statement $A_i$ in the sequence either belongs to a predefined set of axioms of logic or there exists a statement $A_j$ such that both $A_j$ and $A_j \Rightarrow A_i$ occur earlier in a sequence. A statement is provable, if there exists a mathematical proof whose last entry is that statement.

I will not recall here the definition of the set of axioms of logic, which was, of course, the main technical contribution here. At the same time, Church and Turing gave a rigorous definition of a computable function:

Definition. A function $f \colon \mathbb{N} \to \mathbb{N}$ is called computable, if there exists a Turing machine $M$ which, when run on an otherwise empty tape with a binary expansion of a natural number $n$ printed, halts with an otherwise empty tape with a binary expansion of the natural number $f(n)$ printed.

Can AI truly prove anything?

Let us first talk about the relationship between the informal notion of an algorithm, and the formal definition of computability. The philosophical statement that the two notions are equivalent, is known as the Church-Turing thesis. I am not aware of any counterexamples to this thesis being seriously proposed in the literature. Some authors have certainly entertained the possibility of a computing device falling into a black hole finishing the $n$’th step of the computation in $2^{-n}$ seconds, thereby completing an infinite computation in finite time. However, I don’t think that anybody believes in the physical feasibility of such computations: they are merely thought experiments designed to illustrate the blind spots in current physical theories.

The practicality of converting from informal algorithms to Turing machines, and vice versa, is an entirely different question. John von Neumann, while designing ENIAC, assumed that programmers would be low-skilled workers, because the job of converting informal instructions into machine code is purely mechanical. However, von Neumann’s assumption could not be further from the truth. The necessity of reading and modifying programs written by others led to the creation of assembly languages, and eventually high level programming languages. The desire to have a computer run multiple programs consecutively without the programmers coordinating in advance which sections of the memory they were allowed to use led to the invention of operating systems. As a result, by the end of the century, a typical Silicon Valley company had to employ many highly skilled and highly specialized workers in order to create a working software product. Even if the algorithms underlying something like an Uber app are mathematically trivial to describe, the creation of such an app needed a very large amount of man-hours.

On the other hand, the current revolution of artificial intelligence is directly based on creating programs which embody algorithms nobody can understand. Consider the following not quite mathematical questions:

• Does there exist a computable strategy in the game of chess which can beat a human grandmaster?
• Does there exist a computable function which outputs 1 on any picture of a cat and 0 on any picture of a dog?

Nowadays, anybody can use their computer to train a neural network which successfully accomplishes tasks such as these. The resulting program applies a large sequence of matrix multiplications and softmaxes to a digital representation of a picture or a chess position and returns a numerical answer. However, no human can look at these matrices and explain what actual chess insight the neural network uses to beat a human, or what exactly about the curvature of the lines and the color contrast of a picture distinguishes a cat from a dog.

If you look at how people talk about software nowadays, they remain firmly on the ‘formal’ side, not the ‘human understandable’ side. A program is understood as a tangible object which can run on your computer. There still remain some very serious concerns about using programs created by AI agents. If an AI piloting a car leads to a person’s death as a result of an accident, do the creators of the AI bear responsibility? Whatever the reason might be, these legal issues remain largely unresolved, but I’m sure that at some point they will be addressed.

What is a proof?

After this crash course on the history of computers, let us return, finally, to mathematics. Hilbert’s definition of a mathematical proof quickly became the de facto accepted definition of what a proof is. This gave mathematicians a possibility to brag about how mathematics is the only field of human knowledge which deals in completely objective truth. Unlike natural sciences, where the truth depends on believing that somebody did an experiment correctly, and therefore, ultimately, on the consensus of the scientific community, the mathematical proof is absolute.

Of course, all of this was always merely a convenient lie. To my knowledge, no mathematician ever attempted to submit an article with proofs strictly adhering to Hilbert’s system. In reality, most mathematicians will know that the standard axioms for set theory have the acronym ZFC, that Zorn’s lemma is equivalent to the axiom of choice but practically nothing else. One can simply look at the countless statements which changed status over the course of mathematical history to confirm that community consensus is very much a factor in deciding what constitutes a proof:

• The XVII century had seen serious controversy over the fundamental theorem of algebra. Gauss’ thesis of 1799 criticized proofs by d’Alembert and Euler as not rigorous and relying on unproved assumptions. We now know, armed with a rigorous construction of $\mathbb{R}$, that these proofs were correct.
• The Jordan curve theorem carries the name of Camille Jordan, who gave a proof of it in his analysis textbook in 1887. In the XX century, the consensus was that Jordan’s proof was flawed, and the first correct proof is due to Veblen in 1905. Then, in 2007, Hales has written an article defending Jordan’s proof, claiming that the only missing step was proving the theorem for polygons, which is easy. 
• Many fundamental theorems in algebraic geometry carry the names of Enriques, Castelnuovo and Severi. They have published proofs which were at the time accepted in their community, even though the rigorous definitions of some of the basic concepts such as ‘generic point’ were absent from their work. When the rigorous definitions were later supplied by the work of van der Waerden, Noether, Zariski, Weil, many of the Italians’ original proofs became justified.
• Elie Cartan’s original work on differential forms was not rigorous, but when de Rham has given a definition of a differential form, he discovered that all the identities that Cartan gave were correct. Yet people have cited Cartan’s work even before that point in time.

Conversely, when Appel and Haken proved the four-color theorem using computer assistance in 1976, their proof was controversial, because a human could not comprehend this proof in its entirety. Hales’ computer assisted proof of the Kepler conjecture was in review in Annals of Mathematics for seven years. The journal has even considered adding a special editorial note saying that the computer-related parts of the proof could not be verified by the journal’s editors. How would one explain this controversy, if one seriously subscribes to the Hilbert’s notion of a proof? Why would a computer have a problem generating a formal proof considering thousands of cases required? Indeed, both of these controversial proofs eventually received formalizations in Rocq, forcing mathematicians to begrudgingly accept that yes, both the four-color theorems and the Kepler conjecture have a formal proof in the sense of Hilbert, even though no human could understand them.

The classification of finite simple groups presents a different case study. While the proof is not computer assisted, it is very long, combining articles by many different people spanning in total thousands upon thousands of pages. Some mathematicians chose to reject the classification on the grounds that while every part of it was peer reviewed, no single person could possibly understand the proof in its entirety. There is currently no project dedicated to the formalization of the classification, but I’m sure that many mathematicians would begrudgingly accept its correctness if some AI agent produces suitable Lean code tomorrow. Again, from the point of view of Hilbert’s definition, this is very strange. He gave no requirement that the length of a proof should be somehow bounded by a thousand pages. In view of all that, I propose to consider taking the following alternative more seriously:

Definition. A mathematical proof is a text in natural language which explains to a person sufficiently well-trained in mathematics why a certain statement is correct. A statement is mathematically proven, if there is a mathematical proof which is accepted to be correct by sufficiently many well-respected members of the mathematical community.

The elephant in the room

Why am I saying all this? It is because our ego, our frivolous belief in the absoluteness of mathematics is currently being exploited by AI companies in the most cruel way. To them, mathematics is a problem to be solved, not unlike the game of chess. They hold an opinion that if an artificial agent could be created, which is significantly better than humans in producing Hilbert-style proofs, typically written today in the form of Lean code, then surely mathematics becomes a solved endeavor, and mathematicians will become obsolete. But in reality, the story’s not over when a formal proof of a statement is produced by any means necessary. When early programmers wrote pure machine code, they discovered that sometimes other people need to understand their programs in order to read and modify them. Then why, I ask, is it so difficult for us, mathematicians, to articulate why we need to understand the formal proof artifacts in order to practice our art?

To elaborate on my more realistic definition of a proof, I will discuss the following corollary:

Corollary. The statement ‘there exists a complex structure on $S^6$ was not mathematically proven on August 23, 2026.

As it stands, the situation is the following: on August 23, 2026, Claude Fable was prompted to construct a complex structure on a six-dimensional sphere. For reasons I don’t entirely understand, Mr. Fable does not announce his results by himself. Instead, he relies on his flesh puppet Levent Alpöge to announce the results on the personal X account in a maddeningly informal style. As an example of Alpöge’s sense of humor, one can refer to his announcement of the discovery of the Hadamard matrix of order 668. The announcement simply read

+++-+-+-+-+—+—+++-++——++—+—-+—–+++—++-+—+++++++-+–+-+-+–++-+–+–+—-+-+-+-+-++-++—+–++++–++-++++-+++++–+—++-+—$\ldots$

and so on with no accompanying text whatsoever. In this case, Alpöge’s announcement was more human-like:

Please welcome to the world a beautiful new geometric object, to do with a problem i’ve always loved. claude really contains multitudes:D Does $S^6$ admit a complex structure? Yup

Alpöge then asked Fable’s less powerful sibling, Opus, to produce a description of Fable’s construction, which resulted in a 108-page pdf file. The very first page of that file plainly describes a mistake in the 2020 article by Campana, Demailly and Peternell. These authors have claimed to have a proof that the algebraic dimension of a complex manifold homeomorphic to $S^6$ must be zero, whereas Fable’s example has algebraic dimension one. Of course, the whole problem is famous to have inspired countless wrong solutions, so it’s entirely plausible that Campana, Demailly and Peternell has made a mistake. It is also plausible that Fable has made a mistake. It is worth noting that Alpöge himself is a number theorist, not a topologist. It seems that Fable’s construction is not so involved that a number theorist like Alpöge would be unqualified to evaluate it by himself. Yet, it is clear from the context of the announcement that he chose not to engage with the construction seriously, and delegated the work of digesting it to Claude Opus. If the construction is correct, then we have a problem of attribution, not unlike the problem of criminal responsibility for a car crash involving autopilot.

As trivial as the action of prompting Claude is, without Alpöge doing it, the proof wouldn’t have existed. Does Alpöge deserve credit as the discoverer of the complex structure on $S^6$? Qiaochu Yuan claims to have suggested this problem to Alpöge three days before the announcement. Does he deserve some credit as well? What about the team that worked on the development on Claude Fable?

Dealing with artificial mathematics

Because this question infringes on the domain of morality, I do not intend to answer it by supplying hard truths as arguments. Instead, I propose to consider what answer would we like to be accepted in order to benefit society as much as possible? Many mathematicians now wonder whether a day will soon come when an AI will solve the Riemann Hypothesis. So let me indulge in a little thought experiment and try to imagine what the mathematical community’s most likely response will be.

There is no way of knowing whether this hypothetical AI proof will rely on difficult computations, creating new, never before seen theories, or a combination of both. Given that the Riemann Hypothesis have resisted all attempts at proof for over 150 years, the AI proof will almost certainly be very long and difficult. Otherwise, somebody with a human brain would have probably found it already. Let’s say, for the sake of the argument, that AI proof runs for a 1000 pages. Immediately after the announcement, a large conference is organized. All the leading experts in analytic number theory join forces to try and make sense of the gigantic proof. After weeks of hard work, they are able to agree on what a few main insights of the proof are. In a year or two, the Proceedings from the conference are published, condensing the proof to about 500 pages and highlighting its main ideas in a human-readable way.

Now, these mathematicians interpreted the proof because of pure curiosity. In fact, it’s entirely possible that some of them had to compromise their job responsibilities because of it, say, by having to arrange that somebody substitute for the lecture they had to teach on the week of the conference. But the question then becomes: do we need to encourage AI developers to make more proofs, mathematicians to digest them, or a combination of both?

I believe that there are practical reasons to start making the following distinction: when a mathematical statement is known to have a formal proof because an AI system has generated it in Lean, we say that the statement is merely correct. We only say that a statement is mathematically proven, if there is a natural language proof which has been understood at the very least by the field’s leading experts to their satisfaction. I also believe that we should heavily encourage the work which leads to more statements being mathematically proven, and we should discourage the work which only leads to expanding the set of statements known to be merely correct.

My primary justification for this belief is the following: when a future AI system will write the proof of the Riemann Hypothesis, it will inevitably use the language of modern analytic number theory to do so. It would only be possible to understand this proof if you have previously studied analytic number theory, by, for example, reading textbooks written by humans. In a world where the emphasis is on the statements which are merely correct, eventually a point of no return will come. The proof of difficult theorems given by AI would only be able to be understood by another AI. It wouldn’t be impossible to verify that the AI is telling the truth by using Lean as a gold standard of truth in addition to AI cross-examination to obtain high-level descriptions of new mathematical ideas. But if no professional mathematicians are trained in universities, higher mathematics as a language would become extinct. 

The thing is, the language itself is just as valuable, if not more valuable, than knowing that such and such theorems is correct. In fact, the current AI revolution itself only became possible because the researchers in AI labs were trained, among other things, in advanced mathematics. If we were to blindly trust AI in proving our mathematical theorems, how is this meaningfully different from plainly saying that our ideal vision of the future is not ‘Star Trek’, but ‘Idiocracy’?

Conclusion

Fervent AI defenders would of course say that if we have a superintelligent system, then it will have no problem of explaining its genius solutions to the Millennium Problems to us lowly humans, therefore very quickly making them mathematically proven and not just merely correct. First of all, that is not the world we live in. OpenAI feels no obligation to train their most powerful models with a human-readable chain-of-thought, and Levent Alpöge feels no obligation to share Fable’s complete output as it solves the Jacobian conjecture, leaving us completely in the dark. But even if we were to live in that world, I do not believe that delegating all novel problem-solving to AI is a sustainable way of doing mathematics. As a historical comparison, we can look back to the time when calculators were invented. Our society eventually came to the conclusion that kids in elementary school need to learn to perform arithmetic operations by hand and familiarize themselves with its properties. In high school, they are then allowed to shortcut them using calculators, for they are well-equipped to perform sanity checks should they press a wrong button. Would it have mattered if somebody made a calculator with an enormous screen, which gives a complete long division as an output instead of just an answer? 

Currently there are few people that seriously attempt to reconcile human understanding with the current AI climate. Terrence Tao has multiple blogposts dedicated to digestions of whatever result OpenAI or Anthropic decided to work on this week. I believe that he is as good of a digester as he is only because he was already highly skilled in coming up with his own mathematical ideas. It truly does matter that enough mathematics is produced by using natural intelligence, or we risk losing the skill to do so.

Time will tell what the corresponding place of AI in mathematical education and research will be. But one thing is clear to me: prompting GPT Astra to manufacture unreadable Lean proofs for yet another Erdos problem has nothing to do with mathematics whatsoever. If you truly care about mathematics, make sure that mathematics is treated with the respect it deserves. Do not discuss AI-generated texts as if they were mathematical proofs. If you do discuss them, make sure to indicate whether a theorem is currently mathematically proved, merely correct, or, as is sometimes the case, claimed to be “proven” in a completely unverified AI slop file. Make sure that the button mashers from frontier AI labs, who only know the letter ‘X’, and not the letters ‘a’, ‘r’, ‘i’, ‘v’, do not dominate the mathematical discourse. Finally, learn and teach mathematics to make it last through the turbulent years of AI and the centuries beyond.

---

Received 5 September 2026.