What seven mathematicians have said about AI

Most of what I read about AI and math is written by AI people. Labs announce a benchmark score, someone posts a chart, and the conclusion is usually that mathematicians are about to be replaced or already have been. I wanted the other side of the table: what the people who actually prove theorems for a living say, in their own words, with dates attached.

These are public comments from seven mathematicians, rather than a representative survey of the field. The dates matter: their views have developed as the tools have changed. I find the arguments about verification especially useful.

Terence Tao: the collaborator camp

Tao is the most quoted mathematician on this topic, partly because he writes about it constantly and partly because he actually runs experiments in public.

His most cited prediction is from June 2023, in an essay for Microsoft’s AI anthology. He wrote that, combined with tools like formal proof verifiers and symbolic math packages, “2026-level AI, when used properly, will be a trustworthy co-author in mathematical research.”¹ Note the hedges inside that sentence. “When used properly” and “when integrated with tools” are doing a lot of work. He was not predicting that a chatbot alone would co-author papers.

A year later, in a June 2024 interview with Scientific American, he put it more concretely: “I think in three years AI will become useful for mathematicians. It will be a great co-pilot.”² In the same interview he said “I don’t think mathematics will become solved,” though he added that another major AI breakthrough could change that. He also pointed out a specific weakness. Breaking a hard problem into easier pieces is a core skill in research, and he said “AI has not demonstrated any ability to be any better than humans in this regard.”²

The most useful thing Tao has published, in my opinion, is not a prediction but a lab notebook. In September 2024 he posted a thread on Mathstodon about testing an early version of OpenAI’s o1 model. He gave it a complex analysis problem he had worked on before. The model could reach a correct solution with lots of hints, but “did not generate the key conceptual ideas on its own.” He compared the experience to advising “a mediocre, but not completely incompetent, (static simulation of a) graduate student.”³ That parenthetical was added six days after the original post, which is a nice detail: he went back to make the comparison more precise. On September 16 he also apologized for implying that students can be ranked on one scale of competence, and said he meant the comparison only for one narrow kind of research assistance.³ In the same thread he tried using the model to break a Lean formalization task into sublemmas, and said a model like it, fine-tuned on Lean and its math library, could be “extremely useful in formalization projects.”³

By late 2025 Tao had gone from testing chatbots to co-authoring with an AI system as a tool. In November 2025 he was one of four authors (with Bogdan Georgiev, Javier Gómez-Serrano, and Adam Zsolt Wagner) on a paper about Google DeepMind’s AlphaEvolve, an LLM-driven search system that writes and refines programs. The paper presents it as “a tool for autonomously discovering novel mathematical constructions” and tested it on a broad set of problems.⁴ The important word there is constructions. AlphaEvolve finds objects (a better packing, a better example for an inequality) that can be checked directly. It does not write proofs of theorems in the usual sense.

So Tao’s position, as I read it across these three years, is consistent. AI is a collaborator and a tool, its value grows when it is paired with something that checks its work, and it is weakest at the conceptual step of deciding how to attack a problem.

Timothy Gowers: from method skeptic to cautious user

Gowers is more interesting than “early skeptic” suggests, because his skepticism was always about method, not about the destination.

In a 2015 Cambridge lecture titled “What are the prospects for automatic theorem proving?”, his abstract said progress in the field had been “disappointing” and that some approaches “seem to have reached an impasse.” His proposed fix was to “return to the human-oriented approach,” meaning programs that search for proofs the way a human would, instead of exploiting raw speed and memory.⁵

In April 2022 he announced a project along exactly those lines. He described it as “a GOFAI approach” (good old-fashioned AI) and said plainly that it “will not be a machine-learning project,” though he left room for combining the two. He also gave a fairly modest target: theorem provers that would be “genuinely useful” within a few years, at least at the level of a first-year undergraduate.⁶

By July 2024, he was evaluating a different kind of system. In July 2024 he was one of the people who graded Google DeepMind’s AlphaProof on that year’s International Mathematical Olympiad problems, and his comment on one of its solutions was: “The fact that the program can come up with a non-obvious construction like this is very impressive.”⁷

The clearest statement of where he landed is his section of an OpenAI-organized report on GPT-5 and science, posted in November 2025. Gowers wrote: “I have not (yet) had the experience of an LLM making a decisive contribution.” He then listed what it was good for. It found references he suspected existed, it solved small well-defined subproblems in seconds, and it explained why some of his ideas would not work. His downside was specific and, I think, important. When he asked open-ended questions or offered sketchy proof ideas, the model would tell him his ideas worked and produce details that did not “withstand close scrutiny.” His overall verdict was that LLMs “are just beginning to be useful as research collaborators.”⁸

That is close to Tao’s position, but you get there from the opposite direction. Tao started optimistic and added caveats. Gowers started by doubting the machine-learning route and conceded it, without conceding that it has done the hard part yet.

Kevin Buzzard: the verification camp

Buzzard is the mathematician most associated with Lean, the proof assistant most of this ecosystem now runs on. He leads an open-source project at Imperial College London to formalize a proof of Fermat’s Last Theorem in Lean, funded by the UK’s EPSRC until September 2029. The route was planned by Richard Taylor with Buzzard and is a modern variant of the Wiles and Taylor-Wiles proof.⁹ That is a project measured in years and many contributors, and it shapes how he thinks about AI.

His clearest public statement is a December 2024 blog post written after OpenAI’s o3 scored 25 percent on the FrontierMath benchmark. He admitted the result shocked him, because his “mental model on where ‘AI’ is currently, when it comes to doing mathematics, is ‘undergrad or pre-undergrad’.”¹⁰ Then he partly walked the shock back after Elliot Glazer of Epoch AI said on Reddit that a quarter of the problems were “IMO/undergrad style.” Buzzard found that description confusing, given the five public problems. He also made a distinction I found clarifying. FrontierMath questions are “find this number!” questions, while most research mathematics is “prove this theorem!”¹⁰

The core of his argument is about checking. He contrasts two kinds of systems. One writes proofs in a formal language like Lean, and then a grader only has to confirm the statement was translated correctly and the proof compiles. The other writes proofs in English, which a human has to read line by line with no guarantee. He wrote that he was “dreading the inevitable onslaught in a year or two of language model ‘proofs’ of the Riemann hypothesis,” full of vague claims buried in pages of correct math.¹⁰ On the formal side, he wrote: “every time I’ve seen Lean not accept a human argument in the mathematical literature, the human has been wrong.”¹⁰

So Buzzard is not anti-AI. He is anti-unverified-AI. He thinks the generating side will keep improving, and he wants the output in a form a machine can check.

Scholze and Hales: when mathematicians asked computers to check them

Scholze has said much less about AI specifically, and I don’t want to put words in his mouth. But his role in this story is important, because it is a clear case of a top mathematician asking a proof assistant to settle his own doubts about his own result.

In December 2020 he wrote a guest post on Buzzard’s blog proposing what he called the Liquid Tensor Experiment: formalize a key theorem from his work with Dustin Clausen on condensed mathematics. His reason was not curiosity about computers. He considered the theorem foundational, and wrote that “being 99.9% sure is not enough.” He admitted he still had “some small lingering doubts,” and worried that because others would use the result as a black box, “a mistake in this proof could remain uncaught.”¹¹

Six months later, in June 2021, he reported that the project “has verified the entire part of the argument that I was unsure about.” He described Lean as “An assistant in navigating through the thick jungle that this proof is,” and called the result “a landmark achievement.”¹²

None of this is a position on LLMs. What it shows is that a mathematician working at the research frontier found a real use for machine checking on a proof that human readers had not fully checked. That matters for the AI debate, because it is the same need Buzzard is pointing to, coming from someone with no stake in the tooling.

Thomas Hales gives the older version of the same story. In 1998 he and Samuel Ferguson announced a proof of the Kepler conjecture on sphere packing that relied heavily on computer calculations. The referees struggled with it, and the formal proof paper later recorded that the original proof “was published without complete certification from the referees.”¹³ Hales responded by starting the Flyspeck project to formalize the whole thing in the proof assistants HOL Light and Isabelle, which was completed and written up in 2015.

One line from that paper stuck with me: “A proof assistant largely cuts the mathematical referees out of the verification process.”¹³ The paper is careful to add that human oversight is still needed, but for a smaller part of the job.

Hales’s situation in the 2000s is basically the situation everyone is now in with AI-generated proofs. A long argument arrives, mostly correct, too long to check by hand with full confidence. His answer was to formalize. That was a decade-long project for one theorem, which tells you something about the cost.

Martin Hairer: the “no new ideas” camp

Hairer is the most skeptical voice in this survey about AI doing original mathematics. In a July 2025 interview at a congress in Astana, he said AI “does not create knowledge” and “does not create new ideas.” He described how models produce plausible-looking answers, including reference lists where some entries don’t exist: “It sort of makes things up because it makes things plausible.”¹⁴ On AlphaFold, he said “It is very useful, absolutely fantastic work, but it doesn’t provide real understanding.” Asked whether AI would solve most of the century’s scientific problems, he said: “I don’t really believe that.”¹⁴ He also said he doesn’t mind if his students use AI.

He did not stop at commentary. In February 2026, Hairer and ten other mathematicians (including Mohammed Abouzaid, Daniel Spielman, Nikhil Srivastava, and Lauren Williams) posted a paper called “First Proof.” They shared ten questions that had come up naturally in their own research, with answers known to them but kept encrypted for a short time, so AI systems could be tested on problems that were not in any training data.¹⁵

The paper is unusually clear about its own scope. The authors say the experiment “is focused on the final and most well-specified stage of math research, in which the question and frameworks are already understood.” They write that they “do not address the selection of questions to study, the formulation of new definitions, and the development of novel theories.”¹⁵ They use Perelman’s proof of the Poincaré conjecture as an example of how much of the real work came before the final proof.

I think this is the fairest form of the skeptical position. It doesn’t say AI is useless. It says the hard part of math is mostly the part benchmarks can’t measure, and then it builds the best test it can for the part that can be measured.

Alex Kontorovich: formalization is the bottleneck

Kontorovich, a number theorist at Rutgers, wrote the most detailed recent argument I found for where this is all heading. His essay “The Shape of Math To Come” was posted in October 2025.

His main point is that natural-language AI proofs have an error problem that scale won’t fix. He writes that even at 99.99 percent accuracy, “for mathematics, a non-zero error rate creates an unusable tool,” because you can’t tell the right outputs from the wrong ones without checking.¹⁶ So he agrees with Buzzard that verification is the core issue.

But he is also honest about why formalization isn’t a solved answer yet: “As things currently stand, I cannot even state formally most theorems of interest to me, much less prove them.”¹⁶ The formal libraries are too small. His prediction is that with AI helping to formalize, Mathlib “could reach the necessary scale within 5-10 years for many core areas of mathematics.” He compares the eventual switch to the adoption of LaTeX: once writing formally takes less time than writing by hand, he expects “nearly everyone will voluntarily switch to working formally.”¹⁶

That gives a third answer to “what’s the bottleneck?” Hairer’s answer is ideas. Tao’s is the conceptual step of attacking a problem. Kontorovich’s is the library: we can’t check AI output until we can state the math formally, and right now most of research math can’t be stated.

Where they agree, and where they split

Putting all of this side by side, the agreement is wider than the headlines suggest.

Every one of them treats verification as non-negotiable. Scholze wanted more than 99.9 percent. Hales found referees couldn’t fully certify a long computer proof. Buzzard trusts Lean over human arguments. Kontorovich says any nonzero error rate is unusable. Even Tao’s most optimistic prediction is conditional on integration with proof verifiers, and Gowers’s main complaint is that LLMs produce confident details that don’t survive scrutiny. No one in this group is saying “trust the model.”

Several describe useful roles for AI, while the formalization projects show a separate role for proof assistants. Hairer, the biggest skeptic here, lets his students use it and calls AlphaFold fantastic work. Gowers uses it for literature search and small subproblems. Tao co-authored a paper about one.

The splits are in three places.

The first is whether AI will produce original mathematics. Hairer says it doesn’t create new ideas. Tao says it doesn’t yet generate the key concepts but has been improving with each model. Gowers says it hasn’t made a decisive contribution “(yet),” and that parenthetical is a real hedge. Tao’s AlphaEvolve work is an interesting middle case, because a new construction is a kind of discovery, but it is a discovery inside a problem a human set up.

The second is timelines. Tao gave the most specific predictions: a co-pilot within three years of 2024, a trustworthy co-author by 2026 if used properly. Buzzard in late 2024 expected undergraduate-level competence soon and a big jump to research-level ideas as a separate, harder step. Kontorovich gives 5 to 10 years for formal libraries. Hairer gives none in the interview I read.

The third is what the bottleneck is. For Hairer it is ideas, and First Proof is designed around the part that isn’t ideas. For Buzzard and Kontorovich it is verification and the formal libraries that verification needs. For Tao it seems to be integration: the model, the search tools, and the checker working together.

My read

I came away more interested in how these mathematicians would use AI than in whether they sound optimistic about it. There are many possible kinds of help: trying an example, finding a relevant result, checking a step, or suggesting an approach someone hadn’t considered. Each would change a different part of the work.

I’d be excited to see more accounts of what happens after the first promising answer. Can the mathematician make sense of it? Does it lead to a better question? Can someone else build on it? Those details would help me picture the future much more clearly than a prediction about when AI will solve a famous problem.

Sources