The gap between solving a well-posed competition problem and genuinely advancing mathematical knowledge is vast. A new position paper, arXiv:2607.07779, argues that the AI for Mathematics (AI4Math) field has been measuring progress against the wrong targets. Current systems, including the impressive DeepSeek-Prover series and AlphaProof, are fundamentally solvers: given a formally specified goal, they search for a proof. What they cannot do is identify which problems are worth solving, formulate conjectures, or sustain the kind of open-ended mathematical exploration that characterises genuine research. This paper makes the case for redirecting the field toward what the authors call research agents, and it provides a thorough taxonomy of where things currently stand.
Key Contributions
The paper is a position paper with substantial survey content, so its contributions are partly organisational and partly argumentative. The authors offer three main things:
- A unified taxonomy of LLM-based formal mathematics methods, covering training strategies, inference-time reasoning, autoformalization, and agentic workflow design.
- A structured empirical account of AI contributions to open Erdős problems, categorised across six contribution types (primary solutions with no prior work, rediscoveries, partial results, human-AI collaboration, literature review, and formalization).
- An identification of five core barriers separating competition-level solvers from research-grade agents: data and evaluation limitations, absence of relational structure, barriers to mathematical exploration, fragmented tool ecosystems, and inadequate human-AI collaboration frameworks.
The Erdős problem analysis is the most empirically novel section. As of January 2026, the community-maintained tracker records over 4 full AI-primary solutions with no prior known work, 11 or more rediscoveries of known results, and 47 or more AI-formalized proofs. The literature review category is the largest, with over 54 problems receiving AI-assisted bibliographic analysis. These numbers are growing rapidly, with a steep acceleration visible from late 2025 onward, driven by tools like GPT-5 for literature search and Aristotle for formalization.
The Solver-to-Agent Gap
The paper's central thesis is that current systems are architecturally and epistemically unsuited to research mathematics. The argument is convincing, though not entirely new. The distinction between search over a fixed proof space and open-ended conjecture generation has been discussed before, but the authors ground it concretely in the Erdős problem data.
One particularly sharp observation concerns what the successful Erdős solutions have in common: most involve problems where the key insight, once found, leads to a short proof. Problems requiring sustained novel construction or deep structural reasoning remain largely out of reach. This is consistent with what we know about LLM capabilities: strong pattern-matching and proof-search within a well-defined space, but weak generative creativity when the problem itself is underspecified.
The IMO performance data reinforces this picture from a different angle. Systems like Seed-Prover and Gemini Deep Think now achieve gold-medal equivalent scores on IMO 2025, solving five of six problems. Yet the remaining hard problems, typically P3 and P6, continue to resist AI attempts. These are precisely the problems that require novel constructions or ideas that cannot be assembled from known components. The field has, in effect, saturated the retrievable portion of competition mathematics.
Autoformalization and Data Scarcity
A recurring theme is the mismatch in scale between formal and informal corpora. The DeepSeek-Prover training set runs to roughly 3.1 billion tokens of synthetic Lean4 proofs; FineWeb, a general web corpus, is 15 trillion tokens. Fine-tuning datasets for formal mathematics number in the thousands of samples, while informal counterparts run to hundreds of thousands. This is not merely a quantitative gap. Formal proofs require explicit structure that human exposition elides, so a single textbook sentence can expand into dozens of lines of Lean code.
The autoformalization discussion is technically careful. The authors highlight a subtle but important point: syntactic validity does not imply semantic fidelity. The HERALD and Kimina-autoformalizer comparison is instructive here. Both achieve comparable headline performance on MiniF2F, yet downstream automated theorem provers succeed at substantially higher rates on Kimina-autoformalizer outputs. Surface metrics obscure meaningful differences in mathematical correctness.
The Erdős Problem 124 case is a concrete illustration of the specification fidelity problem. Aristotle generated a valid, machine-checked proof, but the formalized statement omitted the greatest common divisor constraint from the original conjecture. The original problem remains open. This kind of silent weakening is particularly dangerous in an autonomous research context, where there may be no human reviewer checking whether the formalized statement matches the intended claim.
Implications and Open Questions
The five-barrier framework the authors propose is a reasonable organising structure, though some barriers are more precisely defined than others. The data and evaluation limitations section is the strongest, with specific examples and quantitative comparisons. The human-AI collaboration section is the weakest, offering general principles without much technical specificity about what improved collaboration architectures would look like in practice.
Several open questions are worth highlighting for researchers in this area:
- How should we evaluate conjecture generation? The paper identifies this as a gap but does not propose concrete metrics. Evaluating whether a conjectured statement is novel, non-trivial, and mathematically interesting is itself a hard problem.
- What does relational structure mean operationally for a theorem prover? The authors argue that current systems lack the ability to reason about dependencies between theorems, but translating this into a training objective or architectural constraint is non-trivial.
- Can synthetic data generation close the formal corpus gap, or does it risk amplifying the biases and gaps already present in the seed library? The curriculum learning approaches described, including AlphaProof's self-generated problem sequences, are promising but their coverage of genuinely novel mathematical territory is unclear.
- The paper notes that AI-generated proofs are often verbose and slow to compile. Automated proof refactoring is mentioned as a direction, but the interaction between conciseness and verifiability is not fully explored.
The broader framing of AI4Math as a potential backbone for scientific discovery across physics, statistics, and optimization is ambitious. The paper gestures at this without providing much evidence that current formal reasoning capabilities transfer to those domains. That said, the argument that mathematical intelligence should be assessed by the ability to move between formal reasoning and real scientific problems is a useful corrective to benchmark-centric evaluation.
Overall, this is a well-organised and technically grounded position paper. The empirical Erdős analysis provides genuine value beyond a standard survey, and the five-barrier taxonomy gives the field a concrete agenda. The fundamental argument, that the field needs to shift from solving specified problems to generating and resolving open ones, is correct and the evidence marshalled here makes it harder to dismiss. Readers working on formal verification, LLM reasoning, or mathematical AI will find it a useful map of where things stand and where the hard problems lie. The full paper is available at https://arxiv.org/abs/2607.07779.