From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

Abstract Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for well-defined mathematical problems through Interactive Theorem Proving (ITP) languages. However, current systems remain fundamentally limited in tackling frontier research mathematics, such as discovering new theorems or resolving open conjectures, which are often open-ended, under-specified, and involve multiple layers of abstraction. We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning. In this position paper, we provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis. More importantly, we identify core limitations of existing systems in serving as mathematical research agents, examining issues across datasets, relational structure, mathematical exploration, tool ecosystem, and human-AI collaboration, outlining a strategic road-map for the future of AI4Math.

Introduction. AI for Mathematics (AI4Math) has long been a central and foundational area of machine intelligence, reflecting the long-standing ambition to endow machines with rigorous formal mathematical reasoning capabilities. Early work in this field focused on neural-symbolic methods [282] designed to integrate neural pattern recognition with the structured logic of Interactive Theorem Proving (ITP) systems. These approaches have achieved notable success in high-accuracy proof synthesis within formal environments [274, 18, 124], but often rely on fixed, manually designed heuristics, limiting their scalability and applicability across diverse mathematical domains [1].

Recently, the emergence of Large Language Models (LLMs) has led to remarkable progress in informal mathematical reasoning. Models like DeepSeek-R1 [57] and the o-series [106] have achieved strong performance on numerous benchmarks [164, 97]. However, these LLM reasoners that generate informal reasoning in natural language are fundamentally limited by the lack of precise, machine-checkable semantics, making their outputs prone to hallucinations [103] and precluding autonomous verification, a prerequisite for tackling open-ended mathematical research.

To bridge this gap, research has been geared towards LLM-driven formal mathematical reasoning systems. By leveraging ITPs such as Lean [50] for rigorous verification, systems including DeepSeek-Prover [55, 267] and Seed-Prover [34] have set new standards for formal proof generation in competition-level mathemat- Despite these strides, we argue that current AI4Math systems still largely operate as solvers, excelling at isolated, well-defined proof generation rather than as researchers capable of expanding the boundaries of mathematical knowledge. While recent systems claim to solve some open problems in Erd ̋os problems, a collection of highly challenging frontier mathematical problems by Paul Erd ̋os, their solutions are largely obtained from rediscovering results already present in the literature [66]. Moreover, these systems still lack the capacity to address many difficult open problems in mathematics, such as the Millennium Prize Problems, which demand genuinely novel ideas, as illustrated in Sec. 4.4 and Table 7. These observations highlight the persistent limitations of existing systems in exploring open-ended research frontiers.

The next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents for frontier mathematics. To substantiate this thesis, we analyze the foundations of the field (Sec. 2), develop a taxonomy of recent approaches (Sec. 3), assess the current state of the art including AI contributions to open Erd ̋os problems (Sec. 4), and identify open challenges that must be addressed to close the gap between competition solvers and research agents (Sec. 5). Our contributions are as follows:

Related work. This section provides necessary background on the historical development of automated theorem proving, the landscape of foundation models for mathematics, and the standard workflow in neural theorem proving.

2.1 Historical Context of Automated Theorem Proving The dream of mechanizing mathematical reasoning predates modern computing by centuries. Gottfried Wilhelm Leibniz’s vision of a calculus ratiocinator in 1666 proposed a universal logical language capable of reducing disputes to calculation, a remarkably prescient anticipation of formal verification. This philosophical aspiration was gradually realized through the development of formal logic in the 19th and 20th centuries, with foundational contributions from Gottlob Frege’s Begriffsschrift, Bertrand Russell and Alfred North Whitehead’s Principia Mathematica, and Kurt Gödel’s incompleteness theorems, which established both the power and inherent limitations of formal systems.

The modern era of automated theorem proving began in earnest with the Logic Theorist [175], developed by Allen Newell, J. C. Shaw, and Herbert A. Simon in 1956. This pioneering system successfully proved 38 of the first 52 theorems from Whitehead and Russell’s Principia Mathematica, demonstrating for the first time that machines could engage in genuine mathematical reasoning. The Logic Theorist employed heuristic search strategies that mimicked aspects of human problem-solving, establishing a paradigm that would influence AI research for decades.

A theoretical breakthrough came in 1965 when John Alan Robinson introduced the resolution principle [197], providing a complete proof procedure for first-order logic. Resolution’s elegance lies in its simplicity: by converting formulas to clausal normal form and repeatedly applying a single inference rule, it can derive any valid conclusion from a set of premises. This work established the foundation for subsequent generations of automated theorem provers and remains influential in modern systems.

The subsequent decades witnessed the development of increasingly sophisticated ATP paradigms, each optimized for different aspects of the theorem proving challenge. Saturation-based provers like E [202], Vampire [119], and SPASS [246] systematically derive consequences from axioms using sophisticated term orderings and redundancy elimination techniques, achieving remarkable efficiency on first-order problems. These systems have won numerous ATP competitions and remain the workhorses of automated reasoning in many application domains.

Method. To better understand the limitations of current approaches and to discuss future directions (see Sec. 5), we review existing neural theorem proving methods, emphasizing LLM-based provers and analyzing them from three complementary perspectives: training strategies, inference-time reasoning mechanisms, and agentic workflow design. Due to their limited generality, geometry-specific methods are deferred to Appendix B.4. Extended technical comparisons and detailed method categorizations are provided in Appendix B.

Supervised Fine-Tuning. LLM-based theorem provers are commonly initialized through supervised finetuning (SFT) on existing proof corpora to acquire basic proof generation capabilities [55, 145, 234, 240]. However, the limited availability of large-scale, high-quality formal proofs in systems such as Lean poses a significant data scarcity challenge, as detailed in Section 5.1. To address this, recent approaches alternatively construct synthetic data at scale. Using DeepSeek-Prover [55] (see illustration in Figure 3) as an example, it mitigates the scarcity of Lean proofs by autoformalizing competition problems and generating 8 million theorem–proof pairs for fine-tuning, while Goedel-Prover [145] addresses it by translating natural-language Reinforcement Learning. Large-scale reinforcement learning (RL) has been shown to enhance the reasoning capabilities of LLMs [57] and has emerged as a core optimization paradigm for LLM-based provers. DeepSeek- Prover-V1.5 [267] introduced RL from proof assistant feedback (RLPAF), in which Lean’s verification of a correct proof provides the reward signal, while subsequent works [145, 146, 234, 105, 81] incorporate last-step RL to further improve performance. Leanabell-Prover series [294, 107] and Xin et al. [268] optimize reasoning trajectories using multi-turn interactions with the verifier. Seed-Prover and DeepSeek-Prover-V2 [34, 196] additionally leverage RL to encourage strong informal chain-of-thought [245] reasoning, facilitating formal proof construction by bridging informal and formal reasoning, while Seed-Prover 1.5 [32] further extends this paradigm with agentic RL through extensive interactions with Lean and other tools.

Search-in-the-loop Training. To push beyond static datasets, many provers employ expert iteration, embedding proof search into the training loop. Early work by Loos et al. [152] demonstrated this clearly by training a deep network to guide clause and inference selection in the first-order prover E [201], turning a high-branching symbolic search into a learned, prioritized exploration process. DeepSeek-AI [55], Li et al. [134], Ambati [6] adopt an iterative bootstrapping approach to gather validated proofs for self-training, whereas Xin et al. [267], Liang et al. [140], Lamont et al. [123] emphasize diversity and exploration within proof tree data. HTPS [124] proposes a graph-based search method to avoid computation on redundant branches, while BFS-Prover [269] explicitly biases the search toward shorter paths. Wu et al. [262] proposes additionally training a critic model to guide the search process and collect proof trajectories. AlphaProof [52] integrates AlphaZero-style [208] self-play training, leveraging policy and value networks to guide Monte Carlo Tree Search and achieving silver-medal–level performance at the 2024 International Mathematical Reflective Learning. Many recent provers emphasize learning from failure by incorporating verifier feedback into training and search. For example, verifier-integrated methods [107, 146, 70] leverage formal error messages and success signals to enable verifier-guided self-correction, turning failed attempts into improved proofs. HybridProver [99] follows a related generate–refine pattern by extracting proof sketches from whole-proof candidates and then refining them stepwise. Complementarily, other approaches emphasize reflective proof structuring. Works such as [232, 62, 303, 302, 307] reward effective subgoal or hypotheses decomposition, while Lyra [304] employs an auxiliary model or verification step to identify errors and guide the prover in repairing them.

Discussion. To bridge the gap between existing problem provers and mathematical research agents, tools that support end-to-end research workflows, from conjecture generation and faithful formalization to proof construction, verification, and interpretation, the field must navigate several critical transitions. We organize these challenges around five strategic pillars: limitations of formal mathematical data (Sec. 5.1), modeling deep relationships across mathematical knowledge (Sec. 5.2), evolving systems from verification to discovery (Sec. 5.3), strengthening integration with external mathematical tools (Sec. 5.4), and enabling effective collaboration between human mathematicians and AI systems (Sec. 5.5).

5.1 Limitations in Formal Math Data and Evaluation Scaling formal mathematical reasoning is fundamentally constrained by the limited supply of high-quality formal proofs. Unlike natural-language corpora, as illustrated in Table 1, formal libraries remain orders of magnitude smaller, pushing the field toward autoformalization as a bridge from informal exposition to machine-verifiable code [249]. Autoformalization confronts a deep semantic mismatch: human mathematics relies on implicit context and shared conventions (e.g., eliding “obvious” bounds or regularity assumptions), while proof assistants require explicit structure. As a result, a single textbook sentence can expand into dozens of lines of formal code, creating a granularity gap that strains current models.

At the same time, AI for mathematics extends beyond formal and informal theorem proving to encompass a broader set of research directions across mathematics and adjacent disciplines, with applications in physics [115, 194], statistics and probability [128], optimization and control [27], and scientific computing [14, 222]. From this perspective, mathematical intelligence should be assessed not only by performance on isolated formal benchmarks, but by the ability to move fluidly between formal reasoning and real scientific problems [235, 89]. This positioning frames AI4Math not merely as a competition solver, but as a research assistant, and potentially a backbone for discovery across domains.

5.2 Shifting from Isolated Proofs to Deep Relationships Current systems operate largely as solvers of isolated math problems, yet the transition to research mathematics demands a shift in focus to the deep relationships that bind theorems into a coherent knowledge graph. Figure 7 illustrates this conceptual framework, showing how relationship-aware representations connect informal concepts, formal lemmas, and tactic-level proof fragments to support abstraction-driven reasoning.

However, this transition is blocked by the combinatorial nightmare of long-horizon proofs; a proof requiring merely 50 steps with a branching factor of 100 generates a search space of 10050 states, making exhaustive search impractical. More broadly, this combinatorial blow-up is a generic feature of subgraph matching formulations. Two recent works [273, 77] tackle this challenge directly, but have not yet been explored in the context of formal mathematics.

To navigate this landscape, recent work increasingly adopts hierarchical planning. Approaches such as Draft-Sketch-Prove [109], hierarchical decomposition [62], and DeepSeek-Prover-V2 [196] mirror human practice by first producing high-level proof sketches, identifying the main subgoals and the intended route, before resolving low-level details. Future systems may require moving beyond flat libraries toward building comprehensive mathematical Knowledge Graphs (KGs) [24] that connect formal concepts, tacticlevel structures, and reusable proof motifs.

Conclusion. In this position paper, we advocate a shift in AI4Math systems from solving predefined problems to acting as research agents for mathematical discovery under rigorous formal reasoning. We summarize the data and methodologies of existing formal mathematics AI systems, with particular emphasis on LLMs-based approaches that have demonstrated significant promise. More importantly, we identify key limitations in building robust AI assistants for mathematical research, spanning datasets, structural reasoning, mathematical exploration, tool ecosystems, and human–AI collaboration, to motivate coherent directions for future work.

Limitations. Several caveats apply to interpreting these results. First, strong selection bias exists: unsuccessful attempts are rarely reported, so success rates cannot be inferred. Second, some “solutions” resolved misformulated versions of problems rather than the intended mathematical claims—illustrating the specification fidelity challenge discussed in Section 5.1. Third, many problems are highly specialized, and the absence of prior solutions may reflect obscurity rather than difficulty. Despite these caveats, the mere existence of AI contributions to open problems posed by Paul Erd ̋os—problems that have stood for decades—represents a qualitative shift in AI mathematical capability.

The pattern of contributions is instructive: most successful full solutions involve problems where the key insight, once found, leads to a relatively short proof. Problems requiring sustained novel construction or deep structural insight remain largely out of reach. This pattern aligns with current LLM capabilities—strong pattern matching and proof search, weaker creative insight generation—and suggests directions for future research.

A core tension of autoformalization is that successful compilation of a formal statement does not ensure semantic correctness. For example, HERALD [74] and Kimina-autoformalizer [234] report comparable headline performance on MiniF2F.