The growing ability of artificial intelligence (AI) to solve mathematical problems is prompting researchers to rethink what constitutes progress in the field. In a lecture at Caltech on October 9, Fields Medallist Terence Tao argued that solving problems, historically one of the most visible goals of mathematical research, is only a means to broader ends. “Further blind optimization of problem-solving alone is now actively harmful to the long-term health of mathematics,” he said in his presentation titled Math 2.0.The debate comes as research institutions move to develop AI for mathematical discovery. On Sunday (October 11), China launched the Yau Laboratory Alliance for Mathematics and Artificial Intelligence at Tsinghua University, bringing together eight institutions and aiming to build a network of over 1,000 scientists working on specialised AI models for mathematics, proof formalisation, and conjecture generation. According to a report by the South China Morning Post, Fields Medallist Shing-Tung Yau noted during a Beijing launch event that China is falling behind the US in applying AI to advance frontier science.For researchers, the challenge is not simply whether AI can generate proofs, but whether those results can be verified, understood and used to advance mathematical knowledge.Vamsi Pritham Pingali, a professor of mathematics at the Indian Institute of Science (IISc), Bengaluru, told The Indian Express that OpenAI’s internal model had already “solved entire research programmes”, affecting young researchers who had little time to adapt.He warned that if a model capable of work at the level of a Fields Medallist became available for $100 a month, “the journal economy will collapse”.Vaishnavi Sundararajan, an Assistant Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology, Delhi, urged caution against both “celebration” and “doomerism”. “Companies like OpenAI are expending millions of dollars’ worth of compute and energy to produce these proofs,” she told The Indian Express, raising questions about whether ordinary academics would have access to comparable systems. She also referred to allegations of plagiarism involving chats considered private, and cautioned that the resulting proofs could still be flawed.In mathematics, it is not enough to find an answer. Researchers must also prove that it is correct.Story continues below this adTake two even numbers: their sum will always be even. Trying this with a few numbers illustrates the pattern, but a proof explains why it must hold every time. Such proofs are the foundation on which mathematicians build new results. An error in one can undermine the work that follows.Yet, checking a proof can be surprisingly difficult. In his book The Proof in the Code, author Kevin Hartnett recounts how mathematician Tom Hales faced this challenge while proving the Kepler conjecture, which concerns the most efficient way to pack spheres together. Hales’s proof involved hundreds of pages of mathematical reasoning and extensive computer calculations. After years of review, referees at Annals of Mathematics were unable to certify the proof as a whole, prompting Hales to look for a way to have a computer check it.Also Read | Navier-Stokes problem: The questions raised by OpenAI’s latest maths ‘breakthrough’The idea draws on a connection between mathematics and computer science. Known as the Curry–Howard correspondence, it relates mathematical propositions to types in computing, and proofs to programs. It underpins tools called proof assistants, which allow mathematicians to encode arguments in a formal language that a computer can check.One such tool is Lean, a functional programming language and interactive theorem prover developed by Leonardo de Moura at Microsoft Research in 2013. It can be used to formalise mathematics and verify software. Mathematicians subsequently adopted it, building a shared digital library of definitions, theorems and proofs that others can reuse rather than start from scratch.Story continues below this ad Terence Tao teaching analytic prime number theory in January 2025 (Wikimedia Commons)But translating a proof into a form a computer understands can itself be a monumental task. Formalising the proof of the Kepler conjecture took about 20 human work-years and produced around 500,000 lines of proof scripts, Hales wrote in a guest post on Terence Tao’s blog on October 9.AI is beginning to ease this bottleneck through autoformalisation — the process of translating mathematical arguments from papers into formal code that a proof assistant can check. An example came in September, when Anthropic said its Claude model had formalised Fermat’s Last Theorem in Lean in 11 days, producing 13 million lines of code. The work followed a simplified version of Andrew Wiles’s existing proof. Its achievement lay in translating an existing proof into a form a computer could check, rather than discovering a new proof.“Autoformalization has become a practical reality in 2026,” Hales wrote.Why does this matter now?On October 6, OpenAI released 722 AI-generated mathematical manuscripts on GitHub, grouped into 372 families of results. The repository now lists 719 after three manuscripts were withdrawn on October 7. A sign error — a mistake involving a positive or negative term in a mathematical expression — in one manuscript invalidated an argument and a construction used by two dependent papers, prompting the withdrawal of all three. OpenAI’s repository says 300 of the 719 top-line results, or about 42%, have been formalised in Lean.Separately, a preprint examining the Lean formalisation accompanying OpenAI’s claimed Navier–Stokes result argued that the formal proof did not correspond to the argument presented in the paper.Story continues below this adAlso in Explained | AI solved an 80-year maths problem. Here’s why this matters beyond mathematicsThe criticism highlights an important distinction: checking whether a formal proof follows a set of rules is not the same as establishing that the formal code faithfully represents the mathematical claim made in the original paper. “Mathematics is, in my view, a social vehicle to discover truths about the world,” Sundararajan said.Elaborating on this distinction, she said, “A proof is, in some sense, not that mathematically valuable as a tangible object,” adding that, “If someone proves a theorem in the woods but nobody can understand it, does it even count as proven?”For her, a mathematical result’s contribution lies not just in the statement itself, but in the intuition it offers, the techniques used to obtain it and the perspectives it opens up for other researchers.On peer review, she said: “One does not simply saddle the community with a whole deluge of unverified proofs, and ask researchers to take on the unpaid labour of painstakingly cross-checking something that might not even be written with human consumption in mind to begin with.”Story continues below this adAn AI model may generate a sequence of mathematical steps, but not every step is necessarily valid, Sundararajan said. Lean can help distinguish valid from invalid steps by checking formalised versions of the arguments. As she explained, “Lean can help separate those with valid steps from the invalid ones by running formalized versions of such ‘proofs’ and checking to see which ones pass.”However, even this process has limits. Sundararajan cautioned that bugs in Lean’s kernel could, if exploited, allow the system to accept invalid reasoning. She also pointed to examples of “junk” theorems that can be proved in Lean, underscoring that passing a formal check does not, by itself, establish a result’s mathematical significance. Given these limitations, as well as the challenge of correctly translating natural-language arguments into formal mathematics, she said, “a Lean proof is not the final stamp of semantic correctness by any means.”Tao described open mathematical problems as “lighthouses” — guides for exploring the mathematical landscape, rather than destinations in themselves. The insights gained through failed attempts and partial progress, he argued, can be more valuable than the final solution. Reaching these problems too quickly through automated tools, he warned, risks disrupting the exploration of alternative approaches and stifling the ideas that might otherwise emerge along the way.