Daniel Litt, a mathematician at the University of Toronto, stated that the current key bottleneck for AI models in mathematics is not text generation, but the inability to reliably verify the correctness of complex derivations; models can write proofs but may not know where the proof fails.

Litt noted that when asked for shorter proofs and then questioned about their correctness, models often deny or correct their previous conclusions; however, when proofs become sufficiently long, containing numerous definitions, lemmas, classifications, and citation chains, errors may be obscured by subsequent text, and the models lack a stable global consistency checking capability.

He mentioned a paper claiming to solve the singularity resolution problem in positive characteristic fields, which is about 800 pages long and generated by AI. This problem is a fundamental challenge in algebraic geometry: the goal is to transform singularities into smooth structures through a series of operations without altering the object's birational structure; there are classical results in the case of characteristic zero, while the positive characteristic case still contains difficult open problems.

Litt stated that he has not yet located specific errors in this 800-page text but believes it cannot constitute a valid proof: if the conclusion were true, it would represent a significant breakthrough in mathematics, and neither human experts have thoroughly reviewed it nor do existing models possess the ability to audit the entire complex proof, track all dependencies, and independently confirm conclusions.

This judgment contrasts with Litt's previous stance on AI's mathematical capabilities. He had previously bet on whether AI could independently write a number theory paper reaching the level of the 2025 Annals of Mathematics by 2030, and after AI demonstrated substantial progress on some mathematical problems, he acknowledged his earlier misjudgment; however, he still views "verifiable long-chain reasoning" as the dividing line from local problem-solving to autonomous mathematical research.

In market mechanisms, funding will prioritize formal verification, theorem provers, proof search, code verification, scientific computing, and high-quality training data infrastructure, rather than simply chasing models that can output longer reasoning texts. Beneficiaries include developers who can integrate model-generated results into machine-checkable systems like Lean, Coq, Isabelle, and institutions with mathematical, engineering, and scientific verification data; those under pressure are products that directly package natural language AI outputs as research conclusions, financial models, or safety-critical code conclusions, as their liability costs will rise rapidly with errors becoming harder to audit.

Source: Public Information