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

# From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
Source: [https://arxiv.org/html/2607.07779](https://arxiv.org/html/2607.07779)
Eric Jiang1,∗, Xiao Liang1,∗, Yikai Zhang1, Yingjia Wan1, Mengting Li1, Haikang Deng1, Alexander K Taylor1, Justin Baker1, Rushil Raghavan1, Junyi Zhang1, Ying Nian Wu1, Andrea L\. Bertozzi1, Kai\-Wei Chang1, Raghu Meka1, Matthew Sottile2, Nanyun Peng1, Amit Sahai1, Terence Tao1, Wei Wang1 1University of California, Los Angeles 2Lawrence Livermore National Laboratory

###### 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\.

![[Uncaptioned image]](https://arxiv.org/html/2607.07779v1/figs/ucla_lawrence/github.png)[Collection of Resources](https://github.com/ericjiang18/Awesome-Formal-Mathematics/tree/main)

††footnotetext:∗Equal contribution\.## 1Introduction

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\[Yuet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib208)\]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\[Yang and Deng,[2019](https://arxiv.org/html/2607.07779#bib.bib12); Bansalet al\.,[2019b](https://arxiv.org/html/2607.07779#bib.bib11); Lampleet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib59)\], but often rely on fixed, manually designed heuristics, limiting their scalability and applicability across diverse mathematical domains\[Abdelazizet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib209)\]\.

Recently, the emergence of Large Language Models \(LLMs\) has led to remarkable progress in informal mathematical reasoning\. Models like DeepSeek\-R1\[DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84)\]and the o\-series\[Jaechet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib81)\]have achieved strong performance on numerous benchmarks\[MAA,[2024](https://arxiv.org/html/2607.07779#bib.bib334); Hendryckset al\.,[2021b](https://arxiv.org/html/2607.07779#bib.bib13)\]\. 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\[Huanget al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib210)\]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\[de Moura and Ullrich,[2021](https://arxiv.org/html/2607.07779#bib.bib52)\]for rigorous verification, systems including DeepSeek\-Prover\[DeepSeek\-AI,[2024a](https://arxiv.org/html/2607.07779#bib.bib17); Xinet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib61)\]and Seed\-Prover\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]have set new standards for formal proof generation in competition\-level mathematics\[Zhenget al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib9)\]\. In parallel, hybrid approaches\[Zhanget al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib44); Chervonyiet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib86)\]that combine LLMs with geometrical deduction engines have surpassed human gold\-medal performance on International Mathematical Olympiad \(IMO\) geometry problems\. These advances highlight LLMs’ potential in generating formal proofs across diverse mathematical domains\.

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ős problems](https://www.erdosproblems.com/), a collection of highly challenging frontier mathematical problems by Paul Erdős, their solutions are largely obtained from rediscovering results already present in the literature\[Erdős,[1957](https://arxiv.org/html/2607.07779#bib.bib197)\]\. Moreover, these systems still lack the capacity to address many difficult open problems in mathematics, such as the[Millennium Prize Problems](https://en.wikipedia.org/wiki/Millennium_Prize_Problems), which demand genuinely novel ideas, as illustrated in Sec\.[4\.4](https://arxiv.org/html/2607.07779#S4.SS4)and Table[7](https://arxiv.org/html/2607.07779#S4.T7)\. 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](https://arxiv.org/html/2607.07779#S2)\), develop a taxonomy of recent approaches \(Sec\.[3](https://arxiv.org/html/2607.07779#S3)\), assess the current state of the art including AI contributions to open Erdős problems \(Sec\.[4](https://arxiv.org/html/2607.07779#S4)\), and identify open challenges that must be addressed to close the gap between competition solvers and research agents \(Sec\.[5](https://arxiv.org/html/2607.07779#S5)\)\. Our contributions are as follows:

1. 1\.Unified analysis of LLM\-based formal mathematics\.We provide a coherent taxonomy covering datasets, autoformalization, training strategies, inference\-time reasoning, and agentic workflows, connecting these threads to identify what current systems can and cannot do\.
2. 2\.Empirical landscape of AI at the research frontier\.We present a systematic account of AI contributions to open Erdős problems, categorized across six contribution types with temporal progression analysis, offering the first structured snapshot of AI capabilities on genuine research\-level mathematics\.
3. 3\.Identification of critical gaps and concrete directions\.We pinpoint five barriers separating competition\-level solvers from research\-grade agents: data and evaluation limitations, lack of relational structure, barriers to mathematical exploration, fragmented tool ecosystems, and inadequate human\-AI collaboration, and propose grounded directions for each\.

## 2Foundations and Preliminaries

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\.1Historical 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\[Newellet al\.,[1956](https://arxiv.org/html/2607.07779#bib.bib241)\], 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\[Robinson,[1965](https://arxiv.org/html/2607.07779#bib.bib242)\], 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\[Schulzet al\.,[2019](https://arxiv.org/html/2607.07779#bib.bib243)\], Vampire\[Kovács and Voronkov,[2013](https://arxiv.org/html/2607.07779#bib.bib244)\], and SPASS\[Weidenbachet al\.,[2007](https://arxiv.org/html/2607.07779#bib.bib245)\]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\.

A parallel development track focused on decision procedures for specific logical theories\. SAT solvers, which determine the satisfiability of propositional formulas, underwent dramatic improvements through techniques like conflict\-driven clause learning \(CDCL\), enabling the solution of industrial problems with millions of variables\. SMT \(Satisfiability Modulo Theories\) solvers like Z3\[De Moura and Bjørner,[2008](https://arxiv.org/html/2607.07779#bib.bib246)\]and CVC5\[Barbosaet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib247)\]extended this success by combining SAT solving with specialized decision procedures for arithmetic, arrays, bit\-vectors, and other theories commonly encountered in software and hardware verification\.

Interactive theorem provers \(ITPs\) emerged as a complementary paradigm, trading full automation for expressive power and human guidance\. Systems like Mizar\[Trybulec,[1993](https://arxiv.org/html/2607.07779#bib.bib248)\], HOL\[Gordon and Melham,[1993](https://arxiv.org/html/2607.07779#bib.bib249)\], Coq\[Team,[2013](https://arxiv.org/html/2607.07779#bib.bib55)\], Isabelle\[Paulson,[1994](https://arxiv.org/html/2607.07779#bib.bib53)\], and Lean\[de Moura and Ullrich,[2021](https://arxiv.org/html/2607.07779#bib.bib52)\]enable human mathematicians to construct machine\-verified proofs of arbitrary complexity, with the computer serving as an infallible checker rather than an autonomous prover\. This human\-machine collaboration has enabled remarkable achievements: the formalization of the Four Color Theorem in Coq\[Gonthier,[2008](https://arxiv.org/html/2607.07779#bib.bib250)\], the verification of the Kepler Conjecture in HOL Light and Isabelle\[Haleset al\.,[2017](https://arxiv.org/html/2607.07779#bib.bib251)\], and the machine\-checked proof of the Odd Order Theorem in Coq\[Gonthieret al\.,[2013](https://arxiv.org/html/2607.07779#bib.bib252)\]\. These landmark projects required years of dedicated effort from expert teams, vividly illustrating both the power of formal verification and the urgent need for better automation—a need that neural approaches now promise to address\.

### 2\.2Formal Mathematics and ITPs

Formal mathematics employs interactive theorem provers \(ITPs\) to provide machine\-checkable correctness guarantees, a capability essential for high\-stakes domains\. The proving process centers on transformingProof States, which comprise the current goals and available hypotheses, into a solved state in which no goals remain usingTactics\. Tactics are state transformation functions such asintro,apply,rewrite, andinduction\. Tactics are validated via the sound inference rules of the foundational logic of the prover\. These systems are supported by extensiveFormal Librarieslike Lean’smathlibThe mathlib Community \[[2020](https://arxiv.org/html/2607.07779#bib.bib57)\]; van Doornet al\.\[[2020](https://arxiv.org/html/2607.07779#bib.bib157)\]and Rocq’smath\-compMahboubi and Tassi \[[2022](https://arxiv.org/html/2607.07779#bib.bib58)\], which provide thousands of definitions and lemmas crucial for premise selection and proof generation\. These libraries are critical to allow mathematicians to work with abstractions above the rarified core foundational logic of the prover\.

Modern ITPs can be categorized by their logical foundations and automation paradigms as follows:

- ❶Dependent Type Theory:Systems like Lean\[de Mouraet al\.,[2015](https://arxiv.org/html/2607.07779#bib.bib39); de Moura and Ullrich,[2021](https://arxiv.org/html/2607.07779#bib.bib52)\]and CoqTeam \[[2013](https://arxiv.org/html/2607.07779#bib.bib55)\]; Bertot and Castéran \[[2013](https://arxiv.org/html/2607.07779#bib.bib54)\]allow for highly expressive proof construction\. Lean has emerged as a central platform for learning\-based research via ecosystems like LeanDojoYanget al\.\[[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\]and TheoremLlamaWanget al\.\[[2024e](https://arxiv.org/html/2607.07779#bib.bib89)\], while Coq supports benchmarks like CoqGymYang and Deng \[[2019](https://arxiv.org/html/2607.07779#bib.bib12)\]\.
- ❷First\-Order Logic \(FOL\):Frameworks like ACL2\[Kaufmann and Moore,[1996](https://arxiv.org/html/2607.07779#bib.bib231)\]are based on FOL with recursive functions and emphasize strong automation\. Additionally, powerful first\-order automated theorem provers, including VampireKovács and Voronkov \[[2013](https://arxiv.org/html/2607.07779#bib.bib244)\]and E\-proverSchulz \[[2002](https://arxiv.org/html/2607.07779#bib.bib236)\], are frequently integrated into ITPs via hammer\-style frameworks to enhance proof automation\.
- ❸Higher\-Order Logic \(HOL\):Systems like Isabelle/HOLPaulson \[[1994](https://arxiv.org/html/2607.07779#bib.bib53)\]emphasize automation through tools likesledgehammerPaulson and Blanchette \[[2012](https://arxiv.org/html/2607.07779#bib.bib91)\]\. This approach has inspired neural\-symbolic systemsJianget al\.\[[2022](https://arxiv.org/html/2607.07779#bib.bib94)\]; McGinness and Baumgartner \[[2024](https://arxiv.org/html/2607.07779#bib.bib168)\]and benchmarks like IsarStepLiet al\.\[[2020](https://arxiv.org/html/2607.07779#bib.bib87)\]and LISAJianget al\.\[[2021](https://arxiv.org/html/2607.07779#bib.bib88)\]\.
- ❹Hybrid Systems:PVSOwreet al\.\[[1992](https://arxiv.org/html/2607.07779#bib.bib237)\]represents a hybrid approach, bridging the gap between HOL and dependent types through its use of predicate subtyping\. This allows for a balance between expressive specification and efficient verification\.
- ❺Set Theory:Metamath\[Megill,[2007](https://arxiv.org/html/2607.07779#bib.bib196); Megill and Wheeler,[2019](https://arxiv.org/html/2607.07779#bib.bib56)\]is a proof framework grounded in ZFC set theory, operating via a minimalist meta\-logic system centered on a single substitution rule\. Its structural simplicity supported early neural theorem proving\[Whalen,[2016](https://arxiv.org/html/2607.07779#bib.bib194); Wang and Deng,[2020](https://arxiv.org/html/2607.07779#bib.bib195); Polu and Sutskever,[2020](https://arxiv.org/html/2607.07779#bib.bib5)\]\.
- ❻Geometry\-Specific Systems:These strategies leverage geometry\-specific languages for deductive and synthetic reasoningChouet al\.\[[1993](https://arxiv.org/html/2607.07779#bib.bib36),[2000](https://arxiv.org/html/2607.07779#bib.bib37)\]based on Wu’s methodsWu \[[2008](https://arxiv.org/html/2607.07779#bib.bib159)\]\. Recent advances, such as AlphaGeometry\[Trinhet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib85)\], integrate neural networks with algebraic reasoning to further enhance proof automation\.

### 2\.3Foundation Models for Mathematical Reasoning

The emergence of large language models has created an entirely new paradigm for mathematical reasoning, one that complements and potentially transforms the classical approaches described above\. We find it useful to categorize the relevant foundation models into several tiers based on their specialization and capabilities\.

At the broadest level, general\-purpose LLMs have demonstrated surprising emergent capabilities in mathematical reasoning despite being trained primarily on general text corpora\. Models like GPT\-4\[Achiamet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib123)\], Claude\[Anthropic,[2024](https://arxiv.org/html/2607.07779#bib.bib125)\], Gemini\[Gemini Teamet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib132); Reidet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib133)\], Llama\[Touvronet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib128); Dubeyet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib127)\], and Qwen\[Yanget al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib130)\]can solve a substantial fraction of undergraduate mathematics problems through in\-context reasoning alone\. The discovery that chain\-of\-thought prompting\[Weiet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib150)\]and even simple prompts like “let’s think step by step”\[Kojimaet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib253)\]can dramatically enhance mathematical performance revealed that these models possess latent reasoning capabilities that appropriate prompting can unlock\. This finding has profound implications for the nature of mathematical reasoning in neural networks and suggests that scale and diverse pretraining data may be sufficient to develop sophisticated problem\-solving abilities\.

A second tier comprises mathematics\-specialized models that undergo continued pretraining on mathematical corpora\. LLEMMA\[Azerbayevet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib95)\]demonstrated that starting from a strong base model and continuing training on a carefully curated mathematical corpus \(including arXiv papers, textbooks, and code\) yields substantial improvements on mathematical benchmarks while preserving general capabilities\. Similarly, DeepSeekMath\[Shaoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib18)\]pushed the boundaries of mathematical reasoning through large\-scale pretraining on mathematical web data, achieving state\-of\-the\-art results on informal mathematics tasks\. These specialized models provide stronger foundations for downstream theorem proving applications\.

The emergence of Large Reasoning Models \(LRMs\) represents perhaps the most dramatic recent development\. Models like o1\[Jaechet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib81)\], o3\[OpenAI,[2025d](https://arxiv.org/html/2607.07779#bib.bib135)\], and DeepSeek\-R1\[DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84)\]demonstrate that extended inference\-time reasoning—where the model generates lengthy internal “thinking” chains before producing answers—can dramatically improve performance on challenging mathematical problems\. DeepSeek\-R1 achieved expert\-level performance on competition mathematics through reinforcement learning that incentivizes productive reasoning chains, suggesting that the combination of sufficient model capacity, appropriate training incentives, and inference\-time computation can yield mathematical reasoning capabilities approaching human expert level\. These developments inform our position that AI systems are now capable of meaningful contributions to formal mathematics, not merely informal problem\-solving\.

Finally, formal mathematics specialists represent systems specifically designed or fine\-tuned for theorem proving in interactive theorem provers\. The lineage begins with GPT\-f\[Polu and Sutskever,[2020](https://arxiv.org/html/2607.07779#bib.bib5)\], which demonstrated that language models could generate valid Metamath proofs and even contribute novel proofs to the library\. Subsequent systems have achieved progressively more impressive results: the DeepSeek\-Prover series\[Xinet al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib60),[b](https://arxiv.org/html/2607.07779#bib.bib61); Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]established new state\-of\-the\-art results through expert iteration and subgoal decomposition; AlphaProof\[DeepMind,[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]achieved silver medal performance at IMO 2024 through massive\-scale reinforcement learning; and open systems like Goedel\-Prover\[Linet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib64),[b](https://arxiv.org/html/2607.07779#bib.bib155)\]and SEED\-Prover\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]have demonstrated that strong formal proving capabilities can be achieved with more accessible computational resources\. This rapid progression motivates our call for the field to pivot toward research\-level formal mathematics, building on these proven capabilities\.

### 2\.4Informal Mathematical Reasoning

While this paper focuses on formal theorem proving with machine\-verified proofs, informal mathematical reasoning, solving problems in natural language, has developed techniques that directly shaped the formal methods discussed in Section[3](https://arxiv.org/html/2607.07779#S3)\. Understanding this lineage clarifies why certain approaches dominate modern theorem provers\.

The foundation lies in chain\-of\-thought prompting: the discovery that intermediate reasoning steps improve mathematical performance\[Weiet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib150); Kojimaet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib253)\]fundamentally shaped how formal provers generate proofs\. Chain\-of\-thought variants\[Zhanget al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib261); Chenet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib262); Wanget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib263); Fuet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib264); Yuet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib176); Lianget al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib180)\]established that decomposing problems into sequential steps, precisely what tactic\-based proving requires, yields dramatic improvements\. The verification methods that followed, including self\-consistency\[Wanget al\.,[2023c](https://arxiv.org/html/2607.07779#bib.bib265)\]and iterative refinement\[Wenget al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib266); Madaanet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib267); Chenet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib103); Shinnet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib105); Linget al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib268); Ling and others,[2023](https://arxiv.org/html/2607.07779#bib.bib269)\], presaged the generate\-verify loops central to systems like HybridProverHuet al\.\[[2025a](https://arxiv.org/html/2607.07779#bib.bib25)\]\.

These ideas extend naturally to structured search\. ToT\[Yaoet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib106)\], GoT\[Bestaet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib270)\], and planning\-based approaches\[Haoet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib271); Zhouet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib272); Dinget al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib273)\]directly inspired the MCTS\-based proof search in HyperTree\[Lampleet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib59)\]and DeepSeek\-Prover\-V1\.5\[Xinet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib61)\]discussed in Section[3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1)\. Similarly, process reward models\[Lightmanet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib274); Uesatoet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib275)\]and automated supervision\[Wanget al\.,[2024d](https://arxiv.org/html/2607.07779#bib.bib276); Luet al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib174); Luoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib277); McAleeseet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib278); Zelikmanet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib279)\]informed how formal systems leverage step\-level feedback, though formal provers enjoy the crucial advantage that proof assistants provide*perfect*verification rather than learned approximations\.

Reinforcement learning \(RL\) techniques that elicit more extensive and precise reasoning\[DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84); Wenet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib175)\]have also been shown transferable to formal reasoning tasks\. Bootstrapping from self\-generated rationales\[Zelikmanet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib279); Gulcehreet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib280); Yuanet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib283); Singhet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib281)\], policy optimization\[Ouyanget al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib282); DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84); Yuet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib116); Yueet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib177)\], and carefully problem curation\[Lianget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib181); Zhaoet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib179); Lianget al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib182); Huanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib178)\]have all been successfully adapted to formal theorem proving\. AlphaProof\[DeepMind,[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]and DeepSeek\-Prover\-V2\[Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]apply these principles with proof assistants replacing learned verifiers, enabling the expert iteration paradigm as discussed in Section[3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1)\.

Progress on informal benchmarks\[Cobbeet al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib284); Hendryckset al\.,[2021b](https://arxiv.org/html/2607.07779#bib.bib13),[a](https://arxiv.org/html/2607.07779#bib.bib285); Clarket al\.,[2018](https://arxiv.org/html/2607.07779#bib.bib286); Heet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib287); Glazeret al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib198); Zenget al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib173); Friederet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib288)\]established evaluation practices now standard in formal proving\. The rapid improvement on MATH, from under 10% to over 90% in three years\[Shaoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib18); DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84)\], demonstrated that scaling laws apply to mathematical reasoning, motivating harder formal benchmarks like PutnamBench \(Section[4](https://arxiv.org/html/2607.07779#S4)\)\. Specialized models\[Lewkowyczet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib289); Luoet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib291); Yuet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib292); Azerbayevet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib95); Shaoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib18); Yanget al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib293); Yinget al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib294); LIet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib295)\]provided pretrained foundations that formal provers build upon\.

Finally, tool integration\[Gaoet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib296); Chenet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib262); Gouet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib297); Wanget al\.,[2024c](https://arxiv.org/html/2607.07779#bib.bib298); Toshniwalet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib144)\]in systems like GPT\-4\[Achiamet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib123)\]and Claude\[Anthropic,[2024](https://arxiv.org/html/2607.07779#bib.bib125)\]established the paradigm that formal provers extend, where the proof assistant becomes the ultimate verification tool\. Multimodal reasoning\[Gaoet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib299); Shiet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib300); Chenet al\.,[2021a](https://arxiv.org/html/2607.07779#bib.bib301); Luet al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib304),[2024e](https://arxiv.org/html/2607.07779#bib.bib305); Zhanget al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib306)\]similarly informs geometric theorem proving like AlphaGeometry\[Trinhet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib85)\], bridging visual and symbolic representations\.

### 2\.5Autoformalization

While early sequence\-to\-sequence modelsWuet al\.\[[2022b](https://arxiv.org/html/2607.07779#bib.bib6)\]; Jianget al\.\[[2022](https://arxiv.org/html/2607.07779#bib.bib94)\]showed promise, data scarcity and alignment costs remain bottlenecksWenget al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib2)\]\. Recent solutions leverage architectural specialization, including multi\-agent pipelines like MASAZhanget al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib23)\], semantic template retrieval via LTRAGHuet al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib24)\], iterative refinement with ReFormChenet al\.\[[2025a](https://arxiv.org/html/2607.07779#bib.bib26)\], and process\-supervised verification using compiler feedbackLuet al\.\[[2024c](https://arxiv.org/html/2607.07779#bib.bib172)\]\. On the evaluation side, FormalAlignLuet al\.\[[2024b](https://arxiv.org/html/2607.07779#bib.bib171)\]automates alignment verification between informal and formal statements via a dual\-loss framework, reducing reliance on manual checking\. Additionally, data synthesis frameworks like ATLASLiuet al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib78)\]and QDTSynthWanget al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib165)\], alongside benchmarks like HeraldGaoet al\.\[[2024](https://arxiv.org/html/2607.07779#bib.bib79)\]and IMO LeanYousefzadehet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib158)\], are actively mitigating data scarcity\.

### 2\.6Standard Workflow in Neural Theorem Proving

![Refer to caption](https://arxiv.org/html/2607.07779v1/x1.png)Figure 1:The Neuro\-Symbolic Interaction Loop\.This diagram illustrates the iterative workflow where the Symbolic Environment \(ITP\) maintains the logical state and provides verifiable feedback \(progress, errors, or completion\), while the Neural Component \(LLM\) acts as a generative policy to construct prompts and predict tactic candidates based on the serialized context\.Neural theorem proving remains a cornerstone of AI4Math\. It is characterized by the interplay between translating informal intent into formal logic and the rigorous execution of proof steps\. This cyclic process relies on the*Symbolic Environment*, such as Interactive Theorem Proving \(ITP\) systems, to ground the*Neural Component*’s reasoning through executable verification and corrective feedback\. In practice, this workflow is typically organized into two interconnected sub\-tasks:AutoformalizationandProof Generation\.

Autoformalizationis the task of translating mathematical problems from natural language descriptions into verifiable formal statements\. This process extends beyond mere syntactic translation, as it requires the resolution of semantic ambiguities, such as implicit bounds, and the bridging of disparate reasoning styles\. An illustration of autoformalization is shown in the left part of Figure[5](https://arxiv.org/html/2607.07779#S3.F5)\. However, the task is primarily hindered by bottlenecks related to data scarcity\[Jianget al\.,[2023a](https://arxiv.org/html/2607.07779#bib.bib403)\]and the difficulty in alignment between informal intent and formal semantics\[Luet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib171); Wenget al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib2); Luet al\.,[2024c](https://arxiv.org/html/2607.07779#bib.bib172)\]\. Extended case studies illustrating common autoformalization challenges are provided in Appendix[C](https://arxiv.org/html/2607.07779#A3)\.

Once the theorem statement is formalized, the system initiates theProof Generationprocess\. This task produces precise symbolic sequences that are verifiable by a symbolic environment through rigorously defined mechanisms for proof construction and validation\. Earlier neural theorem proving approaches\[Wuet al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib93); Jianget al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib94)\]often explicitly decomposed this task into modular sub\-tasks—such as*premise selection*and*tactic generation*—whereas more recent methods, particularly LLM\-based provers\[Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62); Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102); Linet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib155)\], increasingly adopt a unified end\-to\-end paradigm for proof generation in which premise relevance, tactic selection, and long\-horizon reasoning are jointly modeled\. We further detail the taxonomy of the neural provers in Sec\.[3](https://arxiv.org/html/2607.07779#S3)\.

### 2\.7Datasets and Evaluation

LevelDatasetScale \(token/sample\)DescriptionPretrainingFormal pretrainingLEAN\-GitHub\[Wuet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib184)\]1\.3×1081\.3\\times 10^\{8\}tokensLean4 corpus mined from GitHubLeanDojo\-Mathlib\[Yanget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\]1\.4×1081\.4\\times 10^\{8\}tokensLean library theorem–proof pairsDeepseek\-Prover\-Train\[DeepSeek\-AI,[2024a](https://arxiv.org/html/2607.07779#bib.bib17)\]3\.1×1093\.1\\times 10^\{9\}tokensSynthetic Lean4 proofs from math problemsInformal pretrainingFineWeb1\.5×10131\.5\\times 10^\{13\}tokensWeb\-scale natural language textRedPajama\-1T1\.2×10121\.2\\times 10^\{12\}tokensFiltered web \+ books \+ papersThe Pile3\.8×10113\.8\\times 10^\{11\}tokensMixed high\-quality textFine\-tuningFormal fine\-tuningFormalMATH\-All\[Yuet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib77)\]5\.6×1035\.6\\times 10^\{3\}samplesLean4 formal problemsInformal fine\-tuningOpenR1\-Math\-220k4\.5×1054\.5\\times 10^\{5\}samlpesMath problems \+ reasoning traces

Table 1:Scale comparison between formal and informal corpora at pretraining and fine\-tuning levels\. Pretraining scales are reported in tokens; fine\-tuning scales are reported in samples\.Training Data\. Neural theorem proving relies on standardized corpora, most notably the*Lean/mathlib*libraryThe mathlib Community \[[2020](https://arxiv.org/html/2607.07779#bib.bib57)\], which provides a foundation of 1\.3 million lines of formal code\. This corpus is made accessible for machine learning research via*LeanDojo*Yanget al\.\[[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\]and is further augmented by*Lean Workbook*Yinget al\.\[[2024a](https://arxiv.org/html/2607.07779#bib.bib76)\]\. Additionally, efforts within the HOL Light ecosystem, such as*HOList*Paliwalet al\.\[[2019](https://arxiv.org/html/2607.07779#bib.bib92)\], also offer scaled datasets for neural model training and graph\-based representationsPaliwalet al\.\[[2019](https://arxiv.org/html/2607.07779#bib.bib92)\]\.

ITPYearFoundationProof StyleAutomationLibraryML EcosystemIsabelle1986HOLTacticHigh \(Sledgehammer\)AFP \(5M\+ LOC\*\)LISA\[Jianget al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib88)\], IsarStep\[Liet al\.,[2020](https://arxiv.org/html/2607.07779#bib.bib87)\]Coq1989CICTactic/TermMedium383k\+ logical declarations\*CoqGym\[Yang and Deng,[2019](https://arxiv.org/html/2607.07779#bib.bib12)\]HOL Light1996HOLTacticMedium500K\+ LOC\*Holist\[Bansalet al\.,[2019b](https://arxiv.org/html/2607.07779#bib.bib11)\]Metamath2005Set TheoryTermLow40K\+ theorems\*GPT\-f origin\[Polu and Sutskever,[2020](https://arxiv.org/html/2607.07779#bib.bib5)\]Lean 42021CICTacticMediummathlib \(1\.9M\+ LOC\*\)LeanDojo\[Yanget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\], extensive

Table 2:Comparison of Interactive Theorem Provers\. Year indicates first public release\.CIC: Calculus of Inductive Constructions\.HOL: Higher\-Order Logic\.LOC: Lines of Code\.AFP: Archive of Formal Proofs\. \* Library size figures are approximate and reported using ecosystem\-specific metrics\.
### 2\.8Interactive Theorem Prover Comparison

The choice of target ITP significantly impacts neural theorem prover design\. Table[2](https://arxiv.org/html/2607.07779#S2.T2)compares major systems\.

Lean 4 dominates current neural theorem proving research due to mathlib’s comprehensive coverage, LeanDojo’s\[Yanget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\]programmatic interface, and active community development\. Coq offers a longer history with landmark formalizations \(CompCert, Four Color Theorem\) and CoqGym\[Yang and Deng,[2019](https://arxiv.org/html/2607.07779#bib.bib12)\]infrastructure\. Isabelle’s Sledgehammer\[Paulson and Blanchette,[2012](https://arxiv.org/html/2607.07779#bib.bib91)\]provides strong automation by interfacing with external ATPs, inspiring hybrid neural\-symbolic approaches like Thor\[Jianget al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib94)\]\. Metamath’s minimalist explicit\-step design made it an early target for GPT\-f\[Polu and Sutskever,[2020](https://arxiv.org/html/2607.07779#bib.bib5)\], though most subsequent work has moved to more expressive systems\.

BenchmarkOrganizationYearLevelLanguagesSizePrimary FocusminiF2FZhenget al\.\[[2022](https://arxiv.org/html/2607.07779#bib.bib9)\]OpenAI2022HS CompetitionLean, Isa\., MM244Cross\-lingual & competitionProofNetAzerbayevet al\.\[[2023](https://arxiv.org/html/2607.07779#bib.bib10)\]U\. Toronto2023UndergraduateLean185Autoformalization \(Parallel\)PutnamBenchTsoukalaset al\.\[[2024](https://arxiv.org/html/2607.07779#bib.bib74)\]UT Austin2024Uni\. CompetitionLean, Isa\., Coq690Undergraduate reasoningProverBenchRenet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]DeepSeek2025HS \+ UndergradLean325Textbook & AIME problemsCombiBenchLiuet al\.\[[2025a](https://arxiv.org/html/2607.07779#bib.bib75)\]Moonshot AI2025UndergraduateLean100Combinatorial reasoningFormalMathYuet al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib77)\]Sphere AI2025OlympiadLean5,560Olympiad reasoningIneq\-CompZhaoet al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib302)\]Princeton2025IntroductoryLean275Compositional reasoningIneqMathLuet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib303)\]Stanford2025OlympiadLean200Olympiad inequality proofsFATEJianget al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib28)\]Academic2025GraduateLean200Graduate algebraFormal ConjecturesDeepmind \[[2026](https://arxiv.org/html/2607.07779#bib.bib7)\]DeepMindOngoingResearchLean1750\+Research problems

Table 3:Chronological comparison of formal and verifiable benchmarks\.Sizerefers to the number of problems in the test set\.MMdenotes Metamath\.Benchmarks\. To rigorously assess model capabilities across different regimes of difficulty, the community employs a stratified suite of benchmarks\. Among them,*miniF2F*Zhenget al\.\[[2022](https://arxiv.org/html/2607.07779#bib.bib9)\]has long served as a standard for evaluation across multiple ITP systems, featuring Olympiad\-level problems with progressively increasing difficulty, ranging from high\-school to undergraduate mathematics\. As systems advance, evaluation has shifted toward higher\-order reasoning:*PutnamBench*Tsoukalaset al\.\[[2024](https://arxiv.org/html/2607.07779#bib.bib74)\]targets the complexity of undergraduate competitions,*IMO Lean Dataset*Yousefzadehet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib158)\]and*FormalMath*Yuet al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib77)\]consist Olympiad\-level challenges, and*ProofNet*Azerbayevet al\.\[[2023](https://arxiv.org/html/2607.07779#bib.bib10)\]focuses specifically on autoformalization tasks\. These are complemented by specialized benchmarks designed to stress\-test specific capabilities, including textbook comprehension \(*ProverBench*Renet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]\), combinatorics \(*CombiBench*Liuet al\.\[[2025a](https://arxiv.org/html/2607.07779#bib.bib75)\]\), algebra \(*FATE*Jianget al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib28)\]\), inequalities \(*Ineq\-Comp*Zhaoet al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib302)\],*IneqMath*Luet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib303)\]\), and frontier research \(*FrontierMath*\[Glazeret al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib198)\],*Formal Conjectures*\[Deepmind,[2026](https://arxiv.org/html/2607.07779#bib.bib7)\]\)\. Additional details for the benchmarks are provided in Appendix[A\.1](https://arxiv.org/html/2607.07779#A1.SS1), while the evaluation metrics are described in Appendix[A\.3](https://arxiv.org/html/2607.07779#A1.SS3)\. A comparison of interactive theorem provers is presented in Table[2](https://arxiv.org/html/2607.07779#S2.T2)\.

With these foundational concepts established, we now turn to examining the diverse methodological approaches that have been developed for neural theorem proving\.

## 3A Taxonomy of Recent Approaches

\{forest\}

Figure 2:Outline\-style taxonomy of LLM\-based neural theorem proving methods, organized by training strategies, test\-time adaptation, and systematic agent\-prover design\.To better understand the limitations of current approaches and to discuss future directions \(see Sec\.[5](https://arxiv.org/html/2607.07779#S5)\), 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](https://arxiv.org/html/2607.07779#A2.SS4)\. Extended technical comparisons and detailed method categorizations are provided in Appendix[B](https://arxiv.org/html/2607.07779#A2)\.

### 3\.1Training Strategies

#### 3\.1\.1Standard Training Paradigms

Supervised Fine\-Tuning\. LLM\-based theorem provers are commonly initialized through supervised fine\-tuning \(SFT\) on existing proof corpora to acquire basic proof generation capabilities\[DeepSeek\-AI,[2024a](https://arxiv.org/html/2607.07779#bib.bib17); Linet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib64); Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68),[2024e](https://arxiv.org/html/2607.07779#bib.bib89)\]\. 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](https://arxiv.org/html/2607.07779#S5.SS1)\. To address this, recent approaches alternatively construct synthetic data at scale\. Using DeepSeek\-Prover\[DeepSeek\-AI,[2024a](https://arxiv.org/html/2607.07779#bib.bib17)\]\(see illustration in Figure[3](https://arxiv.org/html/2607.07779#S3.F3)\) 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\[Linet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib64)\]addresses it by translating natural\-language problems into Lean to collect 800k proofs and iteratively training provers\. Complementarily, ALCHEMY\[Wuet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib394)\]scales SFT via symbolic mutation, generating large volumes of new formal theorems from existing libraries\.

![Refer to caption](https://arxiv.org/html/2607.07779v1/x2.png)Figure 3:Overview of the DeepSeek\-Prover Framework\.It proceeds in three phases: \(1\)Autoformalization \(& Filtering\)to convert informal problems into high\-quality formal statements; \(2\)Proof Search & Verificationwhere the model generates proof candidates that are rigorously checked by a formal verifier \(e\.g\., Lean\); and \(3\)Training, where successful proofs are used to fine\-tune the policy model for the next iteration\. The KL term in the GRPO loss formulation is omitted\.Reinforcement Learning\. Large\-scale reinforcement learning \(RL\) has been shown to enhance the reasoning capabilities of LLMs\[DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84)\]and has emerged as a core optimization paradigm for LLM\-based provers\. DeepSeek\-Prover\-V1\.5\[Xinet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib61)\]introduced RL from proof assistant feedback \(RLPAF\), in which Lean’s verification of a correct proof provides the reward signal, while subsequent works\[Linet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib64),[b](https://arxiv.org/html/2607.07779#bib.bib155); Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68); Hubertet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib200); Gloeckleet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib104)\]incorporate last\-step RL to further improve performance\. Leanabell\-Prover series\[Zhanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib65); Jiet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib108)\]andXinet al\.\[[2025a](https://arxiv.org/html/2607.07779#bib.bib50)\]optimize reasoning trajectories using multi\-turn interactions with the verifier\. Seed\-Prover and DeepSeek\-Prover\-V2\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102); Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]additionally leverage RL to encourage strong informal chain\-of\-thought\[Weiet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib150)\]reasoning, facilitating formal proof construction by bridging informal and formal reasoning, while Seed\-Prover 1\.5\[Chenet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib170)\]further extends this paradigm with agentic RL through extensive interactions with Lean and other tools\.

#### 3\.1\.2Task\-Specific Strategies

Beyond standard SFT and RL, two task\-specific training strategies for theorem proving have been particularly useful and well studied in the literature\.

Search\-in\-the\-loop Training\. To push beyond static datasets, many provers employ expert iteration, embedding proof search into the training loop\. Early work byLooset al\.\[[2017](https://arxiv.org/html/2607.07779#bib.bib16)\]demonstrated this clearly by training a deep network to guide clause and inference selection in the first\-order proverE\[Schulz,[2002](https://arxiv.org/html/2607.07779#bib.bib236)\], turning a high\-branching symbolic search into a learned, prioritized exploration process\.DeepSeek\-AI \[[2024a](https://arxiv.org/html/2607.07779#bib.bib17)\]; Liet al\.\[[2024a](https://arxiv.org/html/2607.07779#bib.bib70)\]; Ambati \[[2025](https://arxiv.org/html/2607.07779#bib.bib164)\]adopt an iterative bootstrapping approach to gather validated proofs for self\-training, whereasXinet al\.\[[2024b](https://arxiv.org/html/2607.07779#bib.bib61)\]; Lianget al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib27)\]; Lamontet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib233)\]emphasize diversity and exploration within proof tree data\. HTPS\[Lampleet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib59)\]proposes a graph\-based search method to avoid computation on redundant branches, while BFS\-Prover\[Xinet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib63)\]explicitly biases the search toward shorter paths\.Wuet al\.\[[2024a](https://arxiv.org/html/2607.07779#bib.bib69)\]proposes additionally training a critic model to guide the search process and collect proof trajectories\. AlphaProof\[DeepMind,[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]integrates AlphaZero\-style\[Silveret al\.,[2017](https://arxiv.org/html/2607.07779#bib.bib48)\]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 Olympiad\. STP\[Dong and Ma,[2025](https://arxiv.org/html/2607.07779#bib.bib46)\]similarly applies self\-play through iterative conjecture generation and proof attempts for continual self\-training\. Bourbaki\[Zimmeret al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib234)\]further reframes proof search as self\-generated, goal\-conditioned MDPs to better support MCTS\-style exploration\.

Reflective Learning\. Many recent provers emphasize learning from failure by incorporating verifier feedback into training and search\. For example, verifier\-integrated methods\[Jiet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib108); Linet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib155); Firstet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib14)\]leverage formal error messages and success signals to enable verifier\-guided self\-correction, turning failed attempts into improved proofs\. HybridProver\[Huet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib25)\]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\[Wanget al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib66); Donget al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib47); Zhaoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib72),[2023](https://arxiv.org/html/2607.07779#bib.bib71); Zhouet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib109)\]reward effective subgoal or hypotheses decomposition, while Lyra\[Zhenget al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib73)\]employs an auxiliary model or verification step to identify errors and guide the prover in repairing them\. For autoformalization, ReForm\[Chenet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib26)\]adds reflective semantic\-consistency checks to filter or revise formalized statements\.

### 3\.2Test\-time Adaptation

![Refer to caption](https://arxiv.org/html/2607.07779v1/x3.png)Figure 4:Test\-time Adaptation Strategies for LLM\-based Provers\.An overview of various test\-time scaling and adaptation methods, including search algorithms, planning strategies, and retrieval\-augmented approaches that enhance proof generation at inference time\.A promising approach for test\-time scaling in LLM\-based provers is the incorporation of*Search Algorithms*\. However, most search\-based methods have already been discussed in Sec\.[3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1), which integrates search during both training and inference; therefore, this section focuses on test\-time adaptation methods beyond explicit search\.

Planning and Theorem Decomposition\. As the reasoning capabilities of LLMs continue to improve, leveraging them for proof planning or decomposing an original theorem into structured subproblems may offer greater benefits than end\-to\-end proof generation\. DeepTheoremZhanget al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib163)\]operates theorem proving entirely in the informal domain, suggesting the potential of informal reasoning to guide subsequent formal proof generation\. The DSP framework\[Jianget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib15); Caoet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib101)\]streamlines this process by generating an informal proof plan \(Draft\), autoformalizing it into a subgoal\-based skeleton \(Sketch\), and then completing the proof using automated tactics or LLMs \(Prove\)\. Following this line, recent LLM provers\[Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62); Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68); Chenet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib170); Shanget al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib49); Wischermannet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib51)\]favor hybrid settings where informal reasoning is used to guide formal proof generation\. Such informal reasoning is shown to be effective for problem decomposition, facilitating the proof process\[Zhaoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib72),[2023](https://arxiv.org/html/2607.07779#bib.bib71); Zhouet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib109)\]\. For example, DeepSeek\-Prover\-V2\[Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]decomposes a theorem into subgoals, solves each subgoal with a smaller prover, and then stitches the solutions into a complete proof\. Most recently, Hilbert\[Varamballyet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib201)\]adopts a recursive decomposition strategy, pushing the performance ceiling to 99\.2% on MiniF2F\[Zhenget al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib9)\]\. Related decoupled reasoner–prover pipelines\[Lianget al\.,[2025d](https://arxiv.org/html/2607.07779#bib.bib240)\]separate high\-level lemma proposal from low\-level formal verification to tackle harder Olympiad problems\.

Theorem Retrieval\. Since formal mathematics builds heavily on prior results, retrieving relevant theorems and lemmas is a core component of effective theorem proving\. LeanDojo\[Yanget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\], COPRA\[Thakuret al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib232)\], and AlphaProof\[DeepMind,[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]incorporate premise selection by retrieving potentially useful lemmas from large theorem libraries and injecting them into the model context\. Hilbert\[Varamballyet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib201)\]further combines Retrieval\-Augmented Generation \(RAG\) with recursive goal decomposition, repeatedly selecting relevant theorems from a vector database to simplify subgoals\. Beyond static retrieval, ProofNet\+\+\[Ambati,[2025](https://arxiv.org/html/2607.07779#bib.bib164)\]retrieved lemmas using neuro\-symbolic checks, while LeanAgent\[Kumarappanet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib90)\]and LEGO\-Prover\[Wanget al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib67)\]extend retrieval with continual learning by storing previously solved proofs or sub\-proofs, thereby expanding the knowledge base and supporting increasingly complex problems\.

### 3\.3Systematic Agent Prover

![Refer to caption](https://arxiv.org/html/2607.07779v1/x4.png)Figure 5:Agentic formal theorem proving with subgoal caching and parallel verificationAn illustrative workflow in which a natural\-language mathematical statement is autoformalized into a formal theorem, decomposed by a planner into intermediate subgoals, and solved via multiple parallel prover agents\.Recent research increasingly positions LLMs as autonomous agents capable of sophisticated mathematical reasoning, strategic planning, and adaptive behavior\. Drawing on agent\-based AI, this paradigm treats systems as entities that perceive their environment, such as proof states and feedback from ITP systems, to make informed decisions and execute actions toward specific goals\. This agentic model unlocks capabilities absent in simpler systems, particularly regarding multi\-step planning and context\-aware decision\-making\. The latter framework orchestrates an informal reasoning LLM, a formal proof model, and a lemma generation system to substantially extend the capabilities of theorem proving from a single LLM prover\. Aristotle\[Achimet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib199)\]exemplifies a multi\-component agentic pipeline by combining informal lemma generation, Lean proof search, and a dedicated geometry solver at IMO level\. ImProver\[Ahujaet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib393)\]instead treats proof refinement as an agentic rewriting loop, optimizing existing formal proofs under verifier feedback\.

To overcome reasoning bottlenecks, a key feature of agentic systems is to utilize*diverse tools*and*engage with formal environments through standardized interfaces*like LeanDojoYanget al\.\[[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\]and CoqGymYang and Deng \[[2019](https://arxiv.org/html/2607.07779#bib.bib12)\]\. These platforms facilitate feedback loops and hybrid symbolic\-neural execution, while RAG strategies, such as LTRAGHuet al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib24)\]and LemmaHeadYanget al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib19)\], ground generation in existing libraries to effectively reduce the search space\. More comprehensive tool\-use frameworks are realized in systems like Seed\-Prover 1\.5\[Chenet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib170)\], which integrates formal library retrieval alongside general\-purpose computational tools such as Python execution\. PALM\[Luet al\.,[2024d](https://arxiv.org/html/2607.07779#bib.bib35)\]illustrates a complementary generate–then–repair workflow, where LLM drafts are iteratively corrected using symbolic procedures\.

For complex proofs, hierarchical approaches like the Draft\-Sketch\-Prove paradigmJianget al\.\[[2023b](https://arxiv.org/html/2607.07779#bib.bib15)\]; Caoet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib101)\]; Chenet al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib170)\]provide structured workflows by decomposing proofs into manageable subgoals\. A crucial element of this approach is subgoal decomposition\[DeepSeek\-AI,[2024a](https://arxiv.org/html/2607.07779#bib.bib17)\], which identifies intermediate lemmas to simplify the overarching proof process\. Furthermore,*multi\-agent systems*Lianget al\.\[[2025d](https://arxiv.org/html/2607.07779#bib.bib240)\]; Zhanget al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib23)\]enhance this methodology by deploying specialized agents for distinct subgoals in both autoformalization and proof, such as parsing, lemma generation, proving, and verification, highlighting how specialization and collaboration can optimize theorem proving\. Numina\-Lean\-Agent\[Liuet al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib238)\]proposes employing a general\-purpose coding agent that utilizes the Model Context Protocol \(MCP\) to autonomously interact with Lean without task\-specific training\.

By integrating these components, agentic provers have achieved significant breakthroughs, from solving Olympiad inequalitiesLiet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib154)\]; Weiet al\.\[[2024](https://arxiv.org/html/2607.07779#bib.bib156)\]to advancing LLM metacognitive abilitiesDidolkaret al\.\[[2024](https://arxiv.org/html/2607.07779#bib.bib152)\]\. Collectively, these efforts leverage high\-level reasoning, adaptation, and skill composition to push the boundaries of automated theorem proving\.

## 4Current State of the Art

This section documents the current milestones achieved by neural theorem provers across major benchmarks, illustrating the rapid progress in the field and contextualizing the capabilities discussed throughout this paper\.

### 4\.1MiniF2F Benchmark

Table[4](https://arxiv.org/html/2607.07779#S4.T4)shows the progression of state\-of\-the\-art results on MiniF2F\-test, the most widely used benchmark for neural theorem proving\. The benchmark has been effectively saturated by recent systems, with Seed\-Prover\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]achieving 99\.6% \(243/244 problems\), leaving only a single unsolved problem \(IMOSL 2007 Algebra P6\)\. This saturation—from approximately 30% in 2021 to near\-100% in 2025, demonstrates remarkable progress but also highlights the need for more challenging benchmarks\.

SystemModel SizePass RateDateKey TechniqueHilbert\[Varamballyet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib201)\]\-99\.2%Sep 2025Recursive subgoal decompositionSeed\-Prover\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]\-99\.6%Jul 2025Lemma\-style proving, iterative refinementDelta\-Prover\[Zhouet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib109)\]\-95\.5%Jul 2025Long CoT reasoningGoedel\-Prover\-V2\[Linet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib155)\]32B94\.8%Jul 2025\*Scaffolded synthesis, self\-correctionKimina\-Prover\[Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68)\]72B92\.2%Jul 2025\*Large formal reasoning model \+ RLDeepSeek\-Prover\-V2\[Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]671B88\.9%Apr 2025RL for subgoal decompositionProver Agent\[Babaet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib99)\]8B88\.1%Oct 2025Lemma\-guided agent coordination with Lean feedbackDSP\+\[Caoet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib101)\]\-83\.6%Jun 2025Neuro\-symbolic draft–sketch–proveKimina\-Prover\-Preview\[Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68)\]72B80\.7%Apr 2025Large formal reasoning model \+ RLLeanabell\-Prover\-V2\[Jiet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib108)\]7B78\.2%Jul 2025Verifier\-integrated SFT \+ RLBFS\-Prover\[Xinet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib63)\]7B72\.9%Feb 2025Length\-normalized best\-first tree searchHuanyuan\-Prover\[Liet al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib70)\]7B68\.4%Dec 2024Guided tree search with learned criticsInternLM2\.5\-StepProver\[Wuet al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib69)\]7B65\.9%Oct 2024Step\-level supervisionSTP\[Dong and Ma,[2025](https://arxiv.org/html/2607.07779#bib.bib46)\]7B65\.0%Jan 2025Iterative self\-playGoedel\-Prover\[Linet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib64)\]7B64\.7%Feb 2025Massive autoformalization, expert\-iterationDeepSeek\-Prover\-V1\.5\[Xinet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib61)\]7B63\.5%Aug 2024MCTS \+ expert iterationLeanabell\-Prover\[Zhanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib65)\]7B61\.1%Apr 2025Cognitive\-behavior SFT \+ RLInternLM2\-StepProver\[Wuet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib184)\]7B54\.5%Jul 2024Step\-level supervision3D\-Prover\[Lamontet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib233)\]7B53\.1%Oct 2025DPP\-based semantic diversity filtering for tactic selectionLean\-STaR\[Linet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib290)\]7B46\.3%Jul 2024CoT SFT \+ expert\-iterationABEL\[Gloeckleet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib104)\]8B41\.3%Oct 2024Sample\-efficient online RL with HTPSHypertree Proof Search\[Lampleet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib59)\]600M41\.0%Sep 2022MCTS with LLM policyAlchemy\[Wanget al\.,[2024e](https://arxiv.org/html/2607.07779#bib.bib89)\]8B36\.5%Apr 2025Symbolic mutation\-based synthetic theorem generationTheoremLlama\[Wanget al\.,[2024e](https://arxiv.org/html/2607.07779#bib.bib89)\]8B33\.6%Oct 2024NL\-FL bootstrapping \+ curriculum block\-trainingCOPRA\[Thakuret al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib232)\]\-30\.7%Aug 2024Retrieve and in\-context learningProof Artifact Co\-training\[Hanet al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib169)\]837M29\.6%Feb 2021Curriculum learningReProver\[Yanget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\]299M26\.5%Oct 2023Retrieval\-augmented step\-level proving

Table 4:Performance of recent methods on MiniF2F\-test benchmark\. Pass rates represent best reported results under extended inference settings\. Dates marked with \* indicate technical report release dates rather than conference publication dates\.The rapid saturation of MiniF2F illustrates both the success of neural theorem proving methods and the limitations of competition\-level benchmarks\. Problems that seemed intractable just three years ago are now solved reliably, yet the gap to research\-level mathematics remains substantial\.

### 4\.2IMO\-Level Problems

Table[5](https://arxiv.org/html/2607.07779#S4.T5)summarizes AI performance on International Mathematical Olympiad problems, representing the most challenging competition mathematics\. Recent systems have achieved medal\-level performance, with Seed\-Prover solving 5 of 6 problems at IMO 2025\.

SystemAccuracyScoreDateNotesIMO 2025Seed\-Prover\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]83\.3%35/42Jul 2025P1\-5 solved \(P1 post\-competition\)Gemini Deep Think \(IMO Gold\)\[Google DeepMind,[2025](https://arxiv.org/html/2607.07779#bib.bib326)\]83\.3%35/42May 2025P1\-5 solvedGPT\-5\-experimental\*83\.3%35/42Jul 2025P1\-5 solvedGPT\-5 \(high\)\[OpenAI,[2025a](https://arxiv.org/html/2607.07779#bib.bib323)\]38\.1%16/42Jul 2025P1, P3, P4, P5 partially sovledGemini\-2\.5\-Pro\[Comaniciet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib110)\]31\.5%13\.25/42May 2025P1, P3, P4, P5 partially sovledGrok 4 \(specific prompt\)\[xAI,[2025a](https://arxiv.org/html/2607.07779#bib.bib321)\]21\.4%9/42Jul 2025P1\-5 partially sovledo3 \(high\)\[OpenAI,[2025c](https://arxiv.org/html/2607.07779#bib.bib318)\]15\.5%6\.5/42Apr 2025P3\-5 partially sovledDeepseek\-R1\-0528\[DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84)\]7\.1%3/42May 2025P1, P3, P5 partially sovledIMO 2024Gemini Deep Think \(IMO Gold\)\[Google DeepMind,[2025](https://arxiv.org/html/2607.07779#bib.bib326)\]76\.2%32/42Jul 2025\-AlphaProof\[DeepMind,[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]67%28/42Jul 2024Silver medal equivalentGemini Deep Think \(IMO lite\)\[Luonget al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib330)\]40\.5%17/42Aug 2025\-GPT\-5\[OpenAI,[2025a](https://arxiv.org/html/2607.07779#bib.bib323)\]33\.3%14/42Aug 2025\-GPT\-5\-Pro\[OpenAI,[2025a](https://arxiv.org/html/2607.07779#bib.bib323)\]28\.6%12/42Aug 2025\-Gemini\-3\-Pro\-Preview\[Deepmind,[2025](https://arxiv.org/html/2607.07779#bib.bib325)\]18\.6%7\.8/42Nov 2025\-Grok 4\.1 Fast Reasoning\[xAI,[2025b](https://arxiv.org/html/2607.07779#bib.bib322)\]18\.6%7\.8/42Nov 2025\-Grok 4\[xAI,[2025a](https://arxiv.org/html/2607.07779#bib.bib321)\]16\.7%7/42Jul 2025\-GPT\-5\.1\[OpenAI,[2025b](https://arxiv.org/html/2607.07779#bib.bib324)\]7\.1%3/42Nov 2025\-Grok 4 \(heavy\)\[xAI,[2025a](https://arxiv.org/html/2607.07779#bib.bib321)\]7\.1%3/42Jul 2025\-Gemini\-2\.5\-Pro\[Comaniciet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib110)\]7\.1%3/42May 2025\-o4\-mini \(high reasoning\)\[OpenAI,[2025c](https://arxiv.org/html/2607.07779#bib.bib318)\]7\.1%3/42Apr 2025\-o3\[OpenAI,[2025c](https://arxiv.org/html/2607.07779#bib.bib318)\]4\.8%2/42Apr 2025\-Kimi\-K2\-Instruct\[Baiet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib328)\]2\.4%1/42Jul 2025\-Claude Sonnet 4\[Anthropic,[2025](https://arxiv.org/html/2607.07779#bib.bib327)\]2\.4%1/42May 2025\-Claude Opus 4\[Anthropic,[2025](https://arxiv.org/html/2607.07779#bib.bib327)\]2\.4%1/42May 2025\-DeepSeek\-V3\[DeepSeek\-AI,[2024b](https://arxiv.org/html/2607.07779#bib.bib83)\]2\.4%1/42Feb 2025\-DeepSeek\-R1\[DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84)\]0\.0%0/42Jan 2025\-Qwen3\-235B\[Yanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib329)\]0\.0%0/42May 2025\-

Table 5:AI performance on IMO problems\. Seed\-Prover results from\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]; AlphaProof results from\[DeepMind,[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]\. For IMO 2025, additional problem\-level results were obtained from MathArena’s competition view \([https://matharena\.ai/?comp=imo\-\-imo\_2025&view=problem](https://matharena.ai/?comp=imo--imo_2025&view=problem)\)\. For IMO 2024, all results except AlphaProof are taken from\[Luonget al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib330)\]\.GoldandSilverbackground colors indicate official IMO medal\-score thresholds\. Each IMO contest consists of six problems worth seven points each, for a total of 42 points\.The ability to solve 78% of historical IMO problems represents a significant milestone: these problems were designed to challenge the world’s best high school mathematicians, yet AI systems now solve most of them given sufficient compute\. The remaining hard problems \(P3/P6\) continue to pose challenges, often requiring deep insight or novel constructions\.

### 4\.3Erdős Problems: Research\-Level Mathematics

Perhaps the most significant development toward research\-level AI mathematics is the growing list of AI contributions to open problems from the Erdős problem database\.\*\*\*See[https://github\.com/teorth/erdosproblems/wiki/AI\-contributions\-to\-Erdős\-problems](https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems)for a comprehensive and evolving record\.Table[6](https://arxiv.org/html/2607.07779#S4.T6)summarizes these contributions as of January 2026\.

Contribution CategorySolution typeCountExamplesAI primary & no prior knownFull solutions4\+\#205\*, \#543, \#652, \#1051\*Partial results13\+\#42\*, \#75, \#124\*, \#460, \#477\*, \#486, \#514, \#563, \#654, \#665, \#850, \#949\*, \#1040AI primary & later found prior workFull solutions11\+\#281, \#333\*, \#397\*, \#543, \#659, \#728\*, \#851, \#897\*, \#935 \#1026\*, \#1089Partial results4\+\#218, \#635\*, \#935, \#1077\*AI primary & known workFull solutions11\+\#198, \#224\*, \#379, \#493\*, \#652, \#729\*, \#871\*, \#958\*, \#1007\*, \#1043\*, \#1047\*, \#1048\*Partial results13\+\#36, \#43\*, \#264\*, \#488\*, \#507, \#524, \#679, \#788, \#868, \#942, \#951 \#1095\*, \#1097Human\-AI collaborationFull solutions5\+\#347\*, \#401\*, \#659\*, \#848, \#1026\*Partial results6\+\#367, \#460, \#684, \#951, \#1038, \#1141AI\-Powered literature review–54\+\#35, \#66, \#94, \#96, \#124, \#167, \#188, \#203, \#205, \#223, \#248, \#281, \#330, \#333, \#334, \#339, \#347, \#354, \#367, \#370, \#387, \#397, \#401, \#421, \#434, \#481, \#481, \#494, \#515, \#516, \#524, \#543, \#559, \#575, \#591, \#621, \#645, \#652, \#659, \#686, \#689, \#672, \#700, \#705, \#707, \#728, \#729, \#737, \#750, \#786, \#788, \#793, \#811, \#822, \#827, \#829, \#847, \#871, \#903, \#906, \#915, \#940, \#942, \#965, \#967, \#990, \#992,\#1002, \#1008, \#1011, \#1016, \#1019, \#1021, \#1022, \#1038, \#1041, \#1043, \#1044, \#1079, \#1084, \#1099, \#1105, \#1124, \#1129, \#1130, \#1139, \#1148AI\-Formalized proofs–47\+\#26, \#31, \#43, \#56, \#94, \#105, \#106, \#189, \#198, \#226, \#229, \#246, \#275, \#281, \#290, \#303, \#337, \#350, \#367, \#370, \#418, \#480, \#481, \#499, \#541, \#613, \#645, \#659, \#678, \#698, \#707, \#728, \#788, \#845, \#862, \#897, \#958, \#967, \#1000, \#1007, \#1008, \#1022, \#1028, \#1034, \#1036, \#1037, \#1080

Table 6:AI contributions to Erdős problems \(as of January 2026\)\. Counts are approximate due to ongoing updates and classification ambiguity\. Full solutions include cases where literature review later found prior work\. An asterisk \(\*\) in the Examples column indicates results verified or formalized in Lean\. Some results are from Feng’s work\[Fenget al\.,[2026b](https://arxiv.org/html/2607.07779#bib.bib392)\]Figure[6](https://arxiv.org/html/2607.07779#S4.F6)visualizes the cumulative growth of AI contributions across these six categories over time\. The steep acceleration beginning in late 2025, driven first by literature review tools \(GPT\-5\) and formalization systems \(Aristotle\), and then by autonomous provers \(AlphaProof, Aletheia\) in early 2026, illustrates the rapidly expanding scope of AI involvement\. Notably, AI\-formalized proofs and literature reviews account for the largest volumes, while genuinely novel AI\-primary solutions \(with no prior known work\) represent a smaller but growing share\.

![Refer to caption](https://arxiv.org/html/2607.07779v1/x5.png)Figure 6:Cumulative progress of AI contributions to Erdős problems, categorized by contribution type\. Data sourced from the community\-maintained wiki aterdosproblems\.com\(as of April 14, 2026\)\. Numbers in parentheses indicate total unique problems per category\. A single problem may appear in multiple categories\.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](https://arxiv.org/html/2607.07779#S5.SS1)\. 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ős—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\.

Recent systematic efforts have further expanded the landscape of AI contributions to Erdős problems\.Fenget al\.\[[2026a](https://arxiv.org/html/2607.07779#bib.bib397)\]conduct a systematic evaluation of 700 open conjectures using Gemini, resolving 13 problems through semi\-autonomous AI–human collaboration, while the follow\-up Aletheia agent\[Fenget al\.,[2026b](https://arxiv.org/html/2607.07779#bib.bib392)\]autonomously solves additional open questions\. Specific mathematical advances include:Barretoet al\.\[[2026](https://arxiv.org/html/2607.07779#bib.bib400)\]resolve an Erdős–Graham problem on the irrationality of rapidly converging series, with the original proof autonomously generated by the Aletheia AI agent;Ma and Tang \[[2026](https://arxiv.org/html/2607.07779#bib.bib399)\]confirm an Erdős conjecture on random subset sums in finite abelian groups; andLee and Seo \[[2026](https://arxiv.org/html/2607.07779#bib.bib401)\]establish new lower bounds for multivariate independence polynomials using a custom Gemini Deep Think–based research agent\. These results, alongside the broader case studies of AI\-accelerated scientific research\[Woodruffet al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib398)\], illustrate the expanding scope of AI contributions to open mathematical problems while also highlighting the continued reliance on human guidance for problem selection and verification\.

### 4\.4Canonical Lists of Unsolved Problems in Mathematics

Throughout mathematical history, prominent mathematicians have compiled influential lists of open problems that have shaped research directions for decades\. Table[7](https://arxiv.org/html/2607.07779#S4.T7)provides a comprehensive catalog of major problem lists, documenting their scope, current resolution status, and mathematical domains\. These lists serve multiple purposes: they identify frontier questions, communicate priorities across generations, and provide natural benchmarks for measuring progress, making them compelling targets for AI4Math systems\.

For AI4Math research, these lists present both opportunities and challenges\. The Erdős problems, with over 1,100 problems spanning combinatorics and number theory, represent a particularly rich testbed, as evidenced by recent AI contributions documented in Table[6](https://arxiv.org/html/2607.07779#S4.T6)\. However, the most famous open problems \(Riemann Hypothesis, P vs NP, Navier\-Stokes existence and smoothness\) likely require conceptual breakthroughs beyond current AI capabilities, demanding not just proof search but genuine mathematical creativity and novel abstraction\. The First Proof challenge\[Abouzaidet al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib395)\]offers a complementary evaluation paradigm, providing ten never\-before\-published research\-level questions from active mathematicians to objectively assess AI capabilities on problems that require genuine domain expertise rather than retrieval of known solutions\.

Problem ListProposerYearTotalSolvedScope / NotesGeneral / Multi\-DomainHilbert’s Problems\[Hilbert,[1902](https://arxiv.org/html/2607.07779#bib.bib341)\]Hilbert190023∼10\\sim 10Foundations, algebra, geometry, analysis, physicsMillennium Prize\[Carlsonet al\.,[2006](https://arxiv.org/html/2607.07779#bib.bib344)\]Clay Inst\.200071Topology, complexity, analysis, physicsDARPA Math Challenges\[DoD,[2007](https://arxiv.org/html/2607.07779#bib.bib347)\]DARPA2007≥23\\geq 23—Applied mathematics, computationNumber TheoryLandau’s Problems\[Landau,[1912](https://arxiv.org/html/2607.07779#bib.bib342)\]Landau191240Prime distribution conjecturesGuy’s NT Problems\[Guy,[2004](https://arxiv.org/html/2607.07779#bib.bib349)\]Guy1981–2004∼185\\sim 185—All branches of number theoryCombinatorics & Graph TheoryErdős Problems\[Erdős and Graham,[1999](https://arxiv.org/html/2607.07779#bib.bib357)\]Erdős1930s–1996∼1177\\sim 1177††footnotemark:≥475\\geq 475††footnotemark:Combinatorics, graph theory, number theoryErdős–Ko–Rado\[Frankl and Rödl,[1995](https://arxiv.org/html/2607.07779#bib.bib350)\]Various1961–1995∼50\\sim 50—Extremal set theoryBondy–Murty\[Bondy and Murty,[2008](https://arxiv.org/html/2607.07779#bib.bib351)\]Bondy, Murty1976–2008≥100\\geq 100—Structural graph theoryTopology & GeometryThurston’s 24 Questions\[Thurston,[1982](https://arxiv.org/html/2607.07779#bib.bib343)\]Thurston198224∼22\\sim 223\-manifolds, geometric structuresStandard Conjectures\[Grothendieck,[1969](https://arxiv.org/html/2607.07779#bib.bib352)\]Grothendieck196940Algebraic cycles, motivesBass Conjectures\[Quillen,[2006](https://arxiv.org/html/2607.07779#bib.bib354)\]Quillen1973——Algebraic K\-theoryLanglands Program\[Langlands,[1967](https://arxiv.org/html/2607.07779#bib.bib356)\]Langlands1960s\-1970s——Number Theory, Geometry101 Questions\[Gromov,[2017](https://arxiv.org/html/2607.07779#bib.bib355)\]Gromov2017101—Scalar curvatureAnalysis & Dynamical SystemsSmale’s Problems\[Smale,[1998](https://arxiv.org/html/2607.07779#bib.bib345)\]Smale1998≥17\\geq 17≥3\\geq 3Dynamics, complexity, numericsArnold’s Problems\[Arnold,[2005](https://arxiv.org/html/2607.07779#bib.bib348)\]Arnold1956–2003∼861\\sim 861—Dynamical systems, singularitiesMathematical PhysicsSimon Problems\[Simon,[2000](https://arxiv.org/html/2607.07779#bib.bib346)\]Simon2000∼15\\sim 15≥3\\geq 3Schrödinger operators, spectral theory

Table 7:Selected canonical collections of well\-known open problems in mathematics, organized by primary mathematical domain\. Numerical entries are best\-effort estimates compiled from the cited sources and, where noted, non\-archival community trackers\. The symbol∼\\simdenotes an approximate count, and≥\\geqdenotes a documented lower bound\. An em dash \(—\) indicates that no reliable or widely accepted count is available or that "solved" status is not meaningfully tracked\. Counts are reported as of January 2026\.††footnotetext:The counts for Erdős problems are informal estimates based on the community\-maintained websiteerdosproblems\.com\.

## 5Open Challenges and Future Directions

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](https://arxiv.org/html/2607.07779#S5.SS1)\), modeling deep relationships across mathematical knowledge \(Sec\.[5\.2](https://arxiv.org/html/2607.07779#S5.SS2)\), evolving systems from verification to discovery \(Sec\.[5\.3](https://arxiv.org/html/2607.07779#S5.SS3)\), strengthening integration with external mathematical tools \(Sec\.[5\.4](https://arxiv.org/html/2607.07779#S5.SS4)\), and enabling effective collaboration between human mathematicians and AI systems \(Sec\.[5\.5](https://arxiv.org/html/2607.07779#S5.SS5)\)\.

### 5\.1Limitations 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](https://arxiv.org/html/2607.07779#S2.T1), formal libraries remain orders of magnitude smaller, pushing the field toward autoformalization as a bridge from informal exposition to machine\-verifiable codeWenget al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib2)\]\. 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\[Karniadakiset al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib382); Raissiet al\.,[2019](https://arxiv.org/html/2607.07779#bib.bib384)\], statistics and probability\[LeCunet al\.,[2015](https://arxiv.org/html/2607.07779#bib.bib386)\], optimization and control\[Brunton and Kutz,[2024](https://arxiv.org/html/2607.07779#bib.bib381)\], and scientific computing\[Azizzadenesheliet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib379); Thuereyet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib383)\]\. 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\[Wanget al\.,[2023a](https://arxiv.org/html/2607.07779#bib.bib380); Gruetzemacher and Whittlestone,[2022](https://arxiv.org/html/2607.07779#bib.bib385)\]\. This positioning frames AI4Math not merely as a competition solver, but as a research assistant, and potentially a backbone for discovery across domains\.

A core tension of autoformalization is that successful compilation of a formal statement does not ensure semantic correctness\. For example, HERALD\[Gaoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib79)\]and Kimina\-autoformalizer\[Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68)\]report comparable headline performance on MiniF2F\. However, when their outputs are used as inputs to downstream automated theorem provers, state\-of\-the\-art ATP systems achieve markedly higher success rates on statements produced by Kimina\-autoformalizer\. This gap indicates that formalizations are not interchangeable, and surface\-level syntactic validity can mask substantial differences in mathematical fidelity\. Prior analyses of MiniF2F corroborate this issue, documenting cases where problems were unintentionally weakened during formalization, rendering them trivially solvable, or, conversely, made unprovable by subtle translation errorsWanget al\.\[[2025a](https://arxiv.org/html/2607.07779#bib.bib68)\]; Ospanovet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib34)\]\.

Recent months have also seen rapid progress in practical autoformalization, suggesting that systematic formalization is becoming feasible in at least some subfields\. For instance, the Erdős problem database reports that a nontrivial fraction of solved problems now have Lean formalizations, a sharp increase relative to earlier baselines, driven in part by the public availability of Aristotle and improved general\-purpose LLMs\. These gains are encouraging, but they also sharpen the importance of statement\-level fidelity and maintainable proof artifacts as formalization scales\.

Two practical bottlenecks persist:fidelityandefficiency\. First, the*specification gap*undermines end\-to\-end reliability: proof assistants can certify logical consistency, but they do not inherently detect whether a formalized statement faithfully captures the intended theorem\. A subtle mistranslation can make subsequent verification effectively meaningless \(see Appendix[C](https://arxiv.org/html/2607.07779#A3)for concrete examples\)\. This becomes especially salient when LLMs propose solutions to “easy” open problems: the workflow often must include statement verification and literature search, since some purportedly open instances may already be partially \(or fully\) resolved\. For instance, AristotleAchimet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib199)\]reportedly solved Erdős Problem \#124 in late 2025\. While it generated a valid, machine\-checked proof, it targeted a weakened variation of the conjecture that omitted the “greatest common divisor” constraint in the original literature\. The original problem is still open\. Second, AI\-generated proofs are often verbose and slow to compile\. For example, models often list redundant low\-level steps to compensate for uncertainty, resulting in scripts larger than human equivalents\. To scale shared libraries, future systems will need automated agents that refactor bloated proofs into concise, maintainable scripts without sacrificing correctness, ensuring the sustainability of the ever\-growing corpus of formalized mathematics\.

For overcoming the data scarcity, the community is increasingly pivoting toward*synthetic data generation*as a primary lever\. Frameworks such as ATLASLiuet al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib78)\]and QDTSynthWanget al\.\[[2025c](https://arxiv.org/html/2607.07779#bib.bib165)\]use seed models to synthesize diverse training examples from the combinatorial space of statements implied by axioms, while SeedProver\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]leverages relevant conjectures to enrich the training corpus\. Leading systems also move beyond static sampling toward*curriculum learning*: for example, AlphaProofDeepMind \[[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]improves by training on a self\-generated sequence of progressively harder problems, bootstrapping capabilities beyond the initial human demonstrations\. Complementing these approaches, Goedel\-Prover\-V2Linet al\.\[[2025b](https://arxiv.org/html/2607.07779#bib.bib155)\]mitigates data scarcity by mining failed proof trajectories to extract unproven sub\-goals as intermediate training tasks, thereby converting negative feedback into supervision signals\.

### 5\.2Shifting from Isolated Proofs to Deep Relationships

![Refer to caption](https://arxiv.org/html/2607.07779v1/x6.png)Figure 7:A structured mathematical knowledge graph for relationship\-aware reasoning\.A conceptual illustration of a layered mathematical knowledge graph connecting informal mathematical concepts, formal lemmas, and tactic\-level proof fragments\. Such structure enables inexact subgraph matching and abstraction\-based retrieval, allowing provers to exploit recurring proof patterns and deep relationships beyond isolated, flat proof search\.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](https://arxiv.org/html/2607.07779#S5.F7)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 of10050100^\{50\}states, making exhaustive search impractical\. More broadly, this combinatorial blow\-up is a generic feature of subgraph matching formulations\. Two recent worksYanget al\.\[[2023a](https://arxiv.org/html/2607.07779#bib.bib390)\]; Geet al\.\[[2025](https://arxiv.org/html/2607.07779#bib.bib389)\]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\-ProveJianget al\.\[[2023b](https://arxiv.org/html/2607.07779#bib.bib15)\], hierarchical decompositionDonget al\.\[[2024](https://arxiv.org/html/2607.07779#bib.bib47)\], and DeepSeek\-Prover\-V2\[Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]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\)\[Bianet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib203)\]that connect formal concepts, tactic\-level structures, and reusable proof motifs\. With inexact subgraph matching, agentic provers could retrieve recurring patterns across disparate proofs, even when the surface syntax differs or the results exist in different domains\. Moreover, tools such as*anti\-unification*\[Cerna and Kutsia,[2023](https://arxiv.org/html/2607.07779#bib.bib204)\]can abstract these matches into generalized lemmas or “templates”, making shared reasoning structures explicit and thereby reducing the effective search space\.

Operating at the abstraction and structure\-aware reasoning level also benefits from*neuro\-symbolic*integration\. Neural models provide pattern recognition and heuristic guidance, while symbolic automation provides exactness once sub\-goals are precisely stated\. Systems such as HybridProverHuet al\.\[[2025a](https://arxiv.org/html/2607.07779#bib.bib25)\]employ LLMs to guide search and structure tactics, while delegating formally specified obligations to symbolic hammersPaulson and Blanchette \[[2012](https://arxiv.org/html/2607.07779#bib.bib91)\]\. By coordinating neural guidance with symbolic verification over such a structured knowledge graph, future systems may uncover and exploit deeper and more comprehensive structural connections than either paradigm can achieve alone\.

### 5\.3Evolving from Verification to Discovery

The ultimate ambition of AI4Math is to evolve the systems into active discoverers of new mathematical theorems through automated conjecturing\. Emerging frameworks for exploratory proving, such as STPDong and Ma \[[2025](https://arxiv.org/html/2607.07779#bib.bib46)\], address this by employing self\-play loops where agents iteratively conjecture new statements and attempt to prove them, thereby autonomously discovering useful lemmas that expand the frontier of their knowledge\.

![Refer to caption](https://arxiv.org/html/2607.07779v1/x7.png)Figure 8:Overview of the AlphaEvolve Framework in LEAN\.AlphaEvolve showcases mathematical exploration as an evolutionary process in which LLMs propose mutations to formal programs or conjectures, guided by task\-specific scoring functions and verified within a formal environment\.A complementary discovery paradigm employs LLMs as evolutionary mutation operators within program\-search loops, guided by a predefined scoring function that directs the evolution \(Figure[8](https://arxiv.org/html/2607.07779#S5.F8)\)\. Within this paradigm, AlphaEvolve\[Novikovet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib202)\]demonstrates scalable optimization across a wide range of mathematical problems, spanning analysis, combinatorics, geometry, and number theory\[Georgievet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib205)\], and in some Erdős problems discovers bounds beyond previously known human results\. Recent research\[Wanget al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib206); Huet al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib207); Yuksekgonulet al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib239); Jianget al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib402)\]further integrates intermediate generations into model fine\-tuning, improving search efficiency and accelerating the evolutionary process\. However, existing frameworks still expose key limitations for open\-ended mathematical discovery\. Their reliance on problem\-specific scoring functions constrains exploration to variations of predefined objectives, limiting cross\-problem generalization and structural transfer\. In addition, the absence of explicit representations of mathematical relationships across problems prevents the abstraction and reuse of common reasoning patterns\. Most critically, these systems do not support the invention of new concepts or definitions, which often play a central role in reframing problems and enabling major advances\. As a result, while evolutionary approaches scale exploration breadth, they fall short of the conceptual reorganization characteristic of human mathematical discovery\.

Going beyond this, a central challenge is enabling AI to invent new mathematical concepts\. Mathematical approaches such as Grothendieck’s\[McLartyet al\.,[2007](https://arxiv.org/html/2607.07779#bib.bib255)\], which emphasize deep conceptual understanding, intuition, and generalization rather than brute\-force calculation, together with the structuralist emphasis on relations over objects\[Awodey,[2004](https://arxiv.org/html/2607.07779#bib.bib256); Lakatos,[1976](https://arxiv.org/html/2607.07779#bib.bib258)\], suggest that genuine mathematical discovery depends on conceptual reorganization rather than proof search alone\. This perspective aligns naturally with the knowledge\-graph and hierarchical reasoning architectures discussed in Section[5\.2](https://arxiv.org/html/2607.07779#S5.SS2)\. Current systems lack this capacity, marking the boundary between automated theorem provers and true engines of discovery\.

### 5\.4External Tool Integration and Refinement

To act as effective research assistants, AI4Math systems must orchestrate a diverse ecosystem of mathematical tools, much like human mathematicians who combine specialized resources to accelerate discovery\. While ITPs provide absolute soundness, external tools, including Satisfiability Modulo Theories \(SMT\) solvers, Computer Algebra Systems \(CAS\), numerical solvers, and domain\-specific estimators, can substantially speed up proof search, conjecture checking, and intermediate reasoning\[Czajka and Kaliszyk,[2018](https://arxiv.org/html/2607.07779#bib.bib220); Ekiciet al\.,[2017](https://arxiv.org/html/2607.07779#bib.bib221); Mohamedet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib222); Kellison and Appel,[2022](https://arxiv.org/html/2607.07779#bib.bib230)\]\. Realizing this vision requires an agentic workflow that \(i\) decides when to invoke each tool, \(ii\) integrates the results back into a formal environment, and \(iii\) handles failures such as numerical instability, solver incompleteness, or software exceptions\[Schicket al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib215); Yaoet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib216)\]\. Tool\-augmented reasoning has already produced large gains in informal mathematics\[Gouet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib297)\], and delegating subgoals to external provers has long been central to automation in Isabelle/HOL\[Blanchetteet al\.,[2016](https://arxiv.org/html/2607.07779#bib.bib225)\], with recent efforts extending similar capabilities to Lean\[Zhuet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib337)\]\.

A central obstacle in tool integration is the*verification gap*: not all external tools provide evidence that supports their computations\. SMT solvers largely address this issue: when they return satisfying assignment \(SAT\), the SAT can be checked independently; when they return unsatisfying assignment \(UNSAT\), they often provide an unsat\-certificate that constitutes a proof of unsatisfiability\[Barbosaet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib247)\]\. Computer algebra systems, by contrast, typically offer no comparable guarantees\. CAS outputs can be silently incorrect due to bugs, fragile assumption handling, or numerical issues\[Wester,[1999](https://arxiv.org/html/2607.07779#bib.bib372); Stoutemyer,[2014](https://arxiv.org/html/2607.07779#bib.bib376)\], forcing mathematicians to verify results externally\. Closing this gap, by enabling CAS and numerical computations to emit proof certificates suitable for ITP reconstruction, is essential for safely incorporating these tools into formal proof workflows\[Schurret al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib339)\]\.

A promising emerging direction is to augment ITP automation with*equality saturation*and*e\-graphs*\[Willseyet al\.,[2021](https://arxiv.org/html/2607.07779#bib.bib377); Tateet al\.,[2009](https://arxiv.org/html/2607.07779#bib.bib375)\]\. E\-graphs compactly represent large equivalence classes of expressions; given rewrite rules \(e\.g\.,A\+B=B\+AA\+B=B\+A\), saturation explores many rewrite sequences without committing to a single path\. An extraction phase then selects useful representatives, supporting efficient proof reconstruction\. Recent work integrating e\-graphs with Lean\[Rossel,[2024](https://arxiv.org/html/2607.07779#bib.bib378)\]suggests a systematic approach to term rewriting that complements traditional tactic\-based automation\.

Beyond improving how agents*use*tools, strengthening the tools themselves remains underexplored\. Existing SMT solvers and CAS are still constrained in mathematical coverage, proof interpretability, and seamless integration with proof assistants\[Cok and others,[2011](https://arxiv.org/html/2607.07779#bib.bib223); Barbosaet al\.,[2019](https://arxiv.org/html/2607.07779#bib.bib224)\]\. Specialized estimator\-style tools\[Tao,[2024a](https://arxiv.org/html/2607.07779#bib.bib229)\]and genuinely bidirectional CAS–ITP interfaces\[Lewis and Roux,[2022](https://arxiv.org/html/2607.07779#bib.bib340)\]could reduce friction in early\-stage reasoning and make tool outputs easier to formalize\.

Finally, the broader tool ecosystem is highly fragmented: different ITPs expose incompatible frameworks and solver interfaces, forcing agents to master system\-specific invocation protocols\. A unified Proof Agent Interface Protocol \(PAIP\) could standardize access to heterogeneous solver systems and substantially reduce integration barriers\. In parallel, enhancing the ITP itself remains a critical frontier, for example by expanding Lean’s geometric support\[Songet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib227)\]and accelerating its built\-in automation\[Limperg and From,[2023](https://arxiv.org/html/2607.07779#bib.bib228)\]\. Taken together, these challenges suggest that sustained progress in AI4Math will require the co\-evolution of both research agents and the mathematical toolchain they orchestrate\[Blanchetteet al\.,[2016](https://arxiv.org/html/2607.07779#bib.bib225); Avigadet al\.,[2017](https://arxiv.org/html/2607.07779#bib.bib226)\], rather than treating external solvers as fixed black\-box\.

### 5\.5Human and AI4Math System Collaboration

![Refer to caption](https://arxiv.org/html/2607.07779v1/x8.png)Figure 9:Human\-AI Collaboration in Mathematical Research\.An illustration of the collaborative workflow between human mathematicians and AI systems, highlighting the complementary strengths of human insight and AI\-powered automation in formal theorem proving\.We argue that the ultimate goal of AI4Math should not be autonomous theorem proving, but rather collaborative systems that amplify human mathematical ability through tight human\-AI partnership\[Collinset al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib307); Naskręcki and Ono,[2025](https://arxiv.org/html/2607.07779#bib.bib308)\]\. Realizing this vision demands that the community prioritize two underexplored directions: richer interaction paradigms and improved explainability\.

First, the field must develop more effective interaction between humans and theorem\-proving systems\. Code completion tools such as GitHub Copilot\[Chenet al\.,[2021b](https://arxiv.org/html/2607.07779#bib.bib309)\]have transformed software development, yet comparable “proof copilots” for formal mathematics remain limited\[Firstet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib14); Welleck and Saha,[2024](https://arxiv.org/html/2607.07779#bib.bib310)\]\. Effective tactic suggestion requires more than surface\-level pattern matching: it demands an understanding of the current proof state, awareness of relevant lemmas, and the ability to reason about plausible proof strategies\. Early systems such as Copilot for Lean\[Songet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib311)\]and LeanDojo\[Yanget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib8)\]demonstrate that this is possible, but they still fall far short of the smooth, interactive workflows expected by practicing mathematicians\. Numina\-Lean\-Agent\[Liuet al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib238)\]offers a step in this direction through blueprint\-driven human–AI co\-formalization, in which agents and humans jointly guide the structure of a proof\. At the same time, confident hallucinations\[Huanget al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib314)\]and the specification fidelity problem \(Section[5\.1](https://arxiv.org/html/2607.07779#S5.SS1)\) mean that AI suggestions cannot be taken at face value\[Bansalet al\.,[2019a](https://arxiv.org/html/2607.07779#bib.bib313)\]\. We therefore argue that uncertainty estimates\[Kuhnet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib315)\], calibrated confidence\[Kadavathet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib316)\], and explicit disclosure of limitations\[OpenAI,[2024](https://arxiv.org/html/2607.07779#bib.bib317)\]should be built directly into theorem\-proving interfaces, as they are essential for informed human oversight and effective collaboration\.

Second, explainability must be treated as a core requirement rather than a secondary concern\. Machine\-generated proofs are often long and difficult to follow\[Davis,[2023](https://arxiv.org/html/2607.07779#bib.bib312); Friederet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib288); Liet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib1)\], listing many low\-level steps while hiding the main ideas that matter to human mathematicians\. Prior work on proof compression\[Lampleet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib59)\], readable proof generation\[Jianget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib15)\], and the Draft–Sketch–Prove approach\[Wuet al\.,[2022b](https://arxiv.org/html/2607.07779#bib.bib6); Caoet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib101)\]points toward more accessible proof representations\. Human\-in\-the\-loop verification\[Wuet al\.,[2022a](https://arxiv.org/html/2607.07779#bib.bib331)\], especially when combined with personalized feedback\[Zhanget al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib332); Wuet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib333); Tao,[2024b](https://arxiv.org/html/2607.07779#bib.bib335)\], provides an additional path to improving clarity\. The ongoing[Erdős Problems collaboration](https://www.erdosproblems.com/forum/thread/397)captures this collaboration in practice: mathematicians and AI systems \(including ChatGPT, Gemini, and specialized provers like Aristotle and AlphaProof\) have jointly tackled open combinatorics problems, with AI contributing literature reviews, proof formalization, and even novel solution strategies, while humans provide problem selection, correctness verification, and mathematical insight that current systems lack\. This project illustrates both the potential and the current limitations of human\-AI mathematical collaboration: AI tools excel at systematic search but struggle with the creative leaps and contextual judgment that human mathematicians bring\.Woodruffet al\.\[[2026](https://arxiv.org/html/2607.07779#bib.bib398)\]further distill common techniques for effective human\-AI collaboration in scientific research, including iterative refinement, problem decomposition, and deploying AI as an adversarial reviewer, based on case studies spanning theoretical computer science, economics, and optimization\. As a complementary evaluation direction, the First Proof challenge\[Abouzaidet al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib395)\]provides an objective methodology for assessing AI on research\-level mathematics via never\-before\-published problems, with public evaluation efforts\[OpenAI,[2026](https://arxiv.org/html/2607.07779#bib.bib396)\]fostering transparent benchmarking of AI mathematical reasoning capabilities\. We therefore argue that two\-way communication between humans and AI should be a central goal, with systems that explain their reasoning clearly and interfaces that allow users to provide high\-level guidance\[Poluet al\.,[2023](https://arxiv.org/html/2607.07779#bib.bib336)\]\.

## 6Conclusion

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\.

## Acknowledgements

For M\. Sottile, this work was performed under the auspices of the U\.S\. Department of Energy by Lawrence Livermore National Laboratory under Contract DE\-AC52\-07NA27344\. Additionally, we sincerely thank Hengli Li for his valuable assistance in gathering resources and for the insightful discussions that helped shape this work\. We are also grateful to the broader open\-source community, including the maintainers of Lean, mathlib, LeanDojo, and other formal mathematics tools, whose efforts have made much of this research possible\. Finally, we acknowledge the researchers who have made their datasets, benchmarks, and code publicly available, fostering reproducibility and accelerating progress in AI for mathematics\.

## References

- I\. Abdelaziz, M\. Crouse, B\. Makni, V\. Austel, C\. Cornelio, S\. Ikbal, P\. Kapanipathi, N\. Makondo, K\. Srinivas, M\. Witbrock,et al\.\(2022\)Learning to guide a saturation\-based theorem prover\.IEEE Transactions on Pattern Analysis and Machine Intelligence45\(1\),pp\. 738–751\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p1.1)\.
- M\. Abouzaid, A\. J\. Blumberg, M\. Hairer, J\. Kileel, T\. G\. Kolda, P\. D\. Nelson, D\. Spielman, N\. Srivastava, R\. Ward, S\. Weinberger, and L\. Williams \(2026\)First proof\.arXiv preprint arXiv:2602\.05192\.Cited by:[§4\.4](https://arxiv.org/html/2607.07779#S4.SS4.p2.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- J\. Achiam, S\. Adler, S\. Agarwal, L\. Ahmad, I\. Akkaya, F\. L\. Aleman, D\. Almeida, J\. Altenschmidt, S\. Altman, S\. Anadkat,et al\.\(2023\)GPT\-4 technical report\.arXiv preprint arXiv:2303\.08774\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- T\. Achim, A\. Best, A\. Bietti, K\. Der, M\. Fédérico, S\. Gukov, D\. Halpern\-Leistner, K\. Henningsgard, Y\. Kudryashov, A\. Meiburg,et al\.\(2025\)Aristotle: imo\-level automated theorem proving\.arXiv preprint arXiv:2510\.01346\.Cited by:[§C\.1\.3](https://arxiv.org/html/2607.07779#A3.SS1.SSS3.p1.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p1.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p5.1)\.
- ImProver: agent\-based automated proof optimization\.InThe Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24\-28, 2025,External Links:[Link](https://openreview.net/forum?id=dWsdJAXjQD)Cited by:[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p1.1)\.
- M\. Ambati \(2025\)ProofNet\+\+: a neuro\-symbolic system for formal proof verification with self\-correction\.External Links:Arxiv 2505\.24230Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p3.1)\.
- Anthropic \(2024\)Claude 3\.5 sonnet model card addendum\.Note:[https://www\.anthropic\.com](https://www.anthropic.com/)Accessed: November 28, 2024Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- Anthropic \(2025\)Claude opus 4 & claude sonnet 4 system card\.Note:Anthropic Technical ReportCited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.26.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.27.1)\.
- V\. I\. Arnold \(2005\)Arnold’s problems\.Springer Nature\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.11.11.11.2.1.1)\.
- J\. Avigad, J\. Hölzl, and L\. Serafin \(2017\)A formally verified proof of the central limit theorem\.Journal of Automated Reasoning59\(4\),pp\. 389–423\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p5.1)\.
- S\. Awodey \(2004\)An answer to hellman: category theory is a framework for mathematical structuralism\.Philosophia Mathematica\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p3.1)\.
- Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. Avigad \(2023\)ProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.External Links:arXiv 2302\.12433Cited by:[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.3.1)\.
- Z\. Azerbayev, H\. Schoelkopf, K\. Paster, M\. Dos Santos, S\. McAleer, A\. Q\. Jiang, J\. Deng, S\. Biderman, and S\. Welleck \(2024\)LLEMMA: an open language model for mathematics\.arXiv preprint arXiv:2310\.10631\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p3.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- K\. Azizzadenesheli, N\. Kovachki, Z\. Li, M\. Liu\-Schiaffini, J\. Kossaifi, and A\. Anandkumar \(2024\)Neural operators for accelerating scientific simulations and design\.Nature Reviews Physics\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- K\. Baba, C\. Liu, S\. Kurita, and A\. Sannai \(2025\)Prover agent: an agent\-based framework for formal mathematical proofs\.arXiv preprint arXiv:2506\.19923\.Cited by:[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.8.1)\.
- Y\. Bai, Y\. Bao, G\. Chen,et al\.\(2025\)Kimi k2: open agentic intelligence\.arXiv preprint arXiv:2507\.20534\.Cited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.25.1)\.
- G\. Bansal, B\. Nushi, E\. Kamar, D\. S\. Weld, W\. S\. Lasecki, and E\. Horvitz \(2019a\)Beyond accuracy: the role of mental models in human\-ai team performance\.AAAI Conference on Human Computation and Crowdsourcing\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- K\. Bansal, S\. M\. Loos, M\. N\. Rabe, C\. Szegedy, and S\. Wilcox \(2019b\)HOList: an environment for machine learning of higher\-order theorem proving\.International Conference on Machine Learning,pp\. 454–463\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p1.1),[Table 2](https://arxiv.org/html/2607.07779#S2.T2.1.1.4.7)\.
- H\. Barbosa, C\. Barrett, M\. Brain, G\. Kremer, H\. Lachnitt, M\. Mann, A\. Mohamed, M\. Mohamed, A\. Niemetz, A\. Nötzli,et al\.\(2022\)Cvc5: a versatile and industrial\-strength smt solver\.InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems,Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p5.1),[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p2.1)\.
- H\. Barbosa, J\. C\. Blanchette, M\. Fleury, P\. Fontaine, and H\. Schurr \(2019\)Better smt proofs for easier reconstruction\.InAITP 2019\-4th Conference on Artificial Intelligence and Theorem Proving,Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p4.1)\.
- K\. Barreto, J\. Kang, S\. Kim, V\. Kovač, and S\. Zhang \(2026\)Irrationality of rapidly converging series: a problem of Erdős and Graham\.arXiv preprint arXiv:2601\.21442\.Cited by:[§4\.3](https://arxiv.org/html/2607.07779#S4.SS3.p5.1)\.
- Y\. Bertot and P\. Castéran \(2013\)Interactive theorem proving and program development: coq’art: the calculus of inductive constructions\.Springer Science & Business Media\.Cited by:[item ❶](https://arxiv.org/html/2607.07779#S2.I1.ix1.p1.1)\.
- M\. Besta, N\. Blach, A\. Kubicek, R\. Gerstenberger, M\. Podstawski, L\. Gianinazzi, J\. Gajda, T\. Lehmann, H\. Niewiadomski, P\. Nyczyk,et al\.\(2024\)Graph of thoughts: solving elaborate problems with large language models\.AAAI\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- R\. Bian, Y\. Geng, Z\. Yang, and B\. Cheng \(2025\)AutoMathKG: the automated mathematical knowledge graph based on llm and vector database\.Computational Intelligence41\(4\),pp\. e70096\.Cited by:[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p3.1)\.
- J\. C\. Blanchette, C\. Kaliszyk, L\. C\. Paulson, and J\. Urban \(2016\)Hammering towards qed\.Journal of Formalized Reasoning9\(1\),pp\. 101–148\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1),[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p5.1)\.
- J\. A\. Bondy and U\. S\. R\. Murty \(2008\)Graph theory\.Springer\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.7.7.7.2.1.1)\.
- S\. L\. Brunton and J\. N\. Kutz \(2024\)Promising directions of machine learning for partial differential equations\.Nature Computational Science\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- C\. Cao, L\. Song, Z\. Li, X\. Le, X\. Zhang, H\. Xue, and F\. Yang \(2025\)Reviving dsp for advanced theorem proving in the era of reasoning models\.arXiv preprint arXiv:2506\.11487\.Cited by:[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px2.p1.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p3.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.9.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- J\. Carlson, A\. Jaffe, and A\. Wiles \(2006\)The millennium prize problems\.American Mathematical Society\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.13.13.16.1.1.1)\.
- D\. M\. Cerna and T\. Kutsia \(2023\)Anti\-unification and generalization: a survey\.arXiv preprint arXiv:2302\.00277\.Cited by:[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p3.1)\.
- G\. Chen, J\. Wu, X\. Chen, W\. X\. Zhao, R\. Song, C\. Li, K\. Fan, D\. Liu, and M\. Liao \(2025a\)ReForm: reflective autoformalization with prospective bounded sequence optimization\.arXiv preprint arXiv:2510\.24592\.Cited by:[§B\.5](https://arxiv.org/html/2607.07779#A2.SS5.p4.1),[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1)\.
- J\. Chen, W\. Chen, J\. Du, J\. Hu, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, W\. Shi, Z\. Wang, M\. Wang, C\. Wei, S\. Wei, H\. Xin, F\. Yang, W\. Gao, Z\. Yuan, T\. Zhan, Z\. Zheng, T\. Zhou, and T\. H\. Zhu \(2025b\)Seed\-prover 1\.5: mastering undergraduate\-level theorem proving via learning from experience\.External Links:ArXiv 2512\.17260Cited by:[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px1.p1.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p2.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p3.1)\.
- J\. Chen, J\. Tang, J\. Qin, X\. Liang, L\. Liu, E\. P\. Xing, and L\. Lin \(2021a\)GeoQA: a geometric question answering benchmark towards multimodal numerical reasoning\.ACL Findings\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- L\. Chen, J\. Gu, L\. Huang, W\. Huang, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, K\. Ma, C\. Ren, J\. Shen, W\. Shi, T\. Sun, H\. Sun, J\. Wang, S\. Wang, Z\. Wang, C\. Wei, S\. Wei, Y\. Wu, Y\. Wu, Y\. Xia, H\. Xin, F\. Yang, H\. Ying, H\. Yuan, Z\. Yuan, T\. Zhan, C\. Zhang, Y\. Zhang, G\. Zhang, T\. Zhao, J\. Zhao, Y\. Zhou, and T\. H\. Zhu \(2025c\)SEED\-prover: deep and broad reasoning for automated theorem proving\.arXiv preprint arXiv:2507\.23726\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px2.p1.3),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1),[§1](https://arxiv.org/html/2607.07779#S1.p3.1),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1),[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p3.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[§4\.1](https://arxiv.org/html/2607.07779#S4.SS1.p1.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.3.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.3.1.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p6.1)\.
- M\. Chen, J\. Tworek, H\. Jun, Q\. Yuan,et al\.\(2021b\)Evaluating large language models trained on code\.arXiv preprint arXiv:2107\.03374\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- W\. Chen, X\. Ma, X\. Wang, and W\. W\. Cohen \(2023\)Program of thoughts prompting: disentangling computation from reasoning for numerical reasoning tasks\.TMLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- X\. Chen, M\. Lin, N\. Schärli, and D\. Zhou \(2024\)Teaching large language models to self\-debug\.InThe Twelfth International Conference on Learning Representations,Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- Y\. Chervonyi, T\. H\. Trinh, M\. Olšák, X\. Yang, H\. Nguyen, M\. Menegali, J\. Jung, V\. Verma, Q\. V\. Le, and T\. Luong \(2025\)Gold\-medalist performance in solving olympiad geometry with alphageometry2\.arXiv preprint arXiv:2502\.03544\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.SSS0.Px2.p1.1),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1),[§1](https://arxiv.org/html/2607.07779#S1.p3.1)\.
- S\. Chou, X\. Gao, and J\. Zhang \(1993\)Automated production of traditional proofs for theorems in euclidean geometry\.InProceedings of Eigth IEEE Symposium on Login in Computer Science,pp\. 48–56\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p1.1),[item ❻](https://arxiv.org/html/2607.07779#S2.I1.ix6.p1.1)\.
- S\. Chou, X\. Gao, and J\. Zhang \(2000\)A deductive database approach to automated geometry theorem proving and discovering\.Journal of Automated Reasoning25\(3\),pp\. 219–246\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.SSS0.Px2.p1.1),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p1.1),[item ❻](https://arxiv.org/html/2607.07779#S2.I1.ix6.p1.1)\.
- S\. Chou \(1988\)An introduction to wu’s method for mechanical theorem proving in geometry\.Journal of Automated Reasoning4\(3\),pp\. 237–267\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p1.1)\.
- P\. Clark, I\. Cowhey, O\. Etzioni, T\. Khot, A\. Sabharwal, C\. Schoenick, and O\. Tafjord \(2018\)Think you have solved question answering? try arc, the ai2 reasoning challenge\.arXiv preprint\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano,et al\.\(2021\)Training verifiers to solve math word problems\.arXiv preprint\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- D\. R\. Coket al\.\(2011\)The smt\-libv2 language and tools: a tutorial\.Language c,pp\. 2010–2011\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p4.1)\.
- K\. Collins, I\. Sucholutsky, B\. Umang,et al\.\(2024\)Building machines that learn and think with people\.Nature Human Behaviour\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p1.1)\.
- G\. Comanici, E\. Bieber, M\. Schaekermann, I\. Pasupat, N\. Sachdeva, I\. Dhillon, M\. Blistein, O\. Ram, D\. Zhang, E\. Rosen,et al\.\(2025\)Gemini 2\.5: pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities\.arXiv preprint arXiv:2507\.06261\.Cited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.22.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.7.1)\.
- Ł\. Czajka and C\. Kaliszyk \(2018\)Hammer for coq: automation for dependent type theory\.Journal of automated reasoning61\(1\),pp\. 423–453\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- E\. Davis \(2023\)Mathematics, word problems, common sense, and artificial intelligence\.Arxiv preprint 2301\.09723\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- L\. De Moura and N\. Bjørner \(2008\)Z3: an efficient smt solver\.InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems,Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p5.1)\.
- L\. de Moura, S\. Kong, J\. Avigad, F\. Van Doorn, and J\. von Raumer \(2015\)The lean theorem prover \(system description\)\.InInternational Conference on Automated Deduction,pp\. 378–388\.Cited by:[item ❶](https://arxiv.org/html/2607.07779#S2.I1.ix1.p1.1)\.
- L\. de Moura and S\. Ullrich \(2021\)The lean 4 theorem prover and programming language\.InAutomated Deduction–CADE 28,pp\. 625–635\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p1.1),[§1](https://arxiv.org/html/2607.07779#S1.p3.1),[item ❶](https://arxiv.org/html/2607.07779#S2.I1.ix1.p1.1),[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- DeepMind \(2024\)AI achieves silver\-medal standard solving international mathematical olympiad problems\.Note:[https://deepmind\.google/discover/blog/ai\-solves\-imo\-problems\-at\-silver\-medal\-level/](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px2.p1.3),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p3.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.13.1.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p6.1)\.
- Deepmind \(2025\)Gemini 3 system card\.Note:Deepmind Technical ReportCited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.17.1)\.
- Deepmind \(2026\)Formal Conjectures: A collection of formalized statements of conjectures in Lean\.GitHub\.Note:[https://github\.com/google\-deepmind/formal\-conjectures](https://github.com/google-deepmind/formal-conjectures)Accessed: 2026\-01\-22Cited by:[§A\.1](https://arxiv.org/html/2607.07779#A1.SS1.p3.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.11.1)\.
- DeepSeek\-AI \(2024a\)DeepSeek\-prover: advancing theorem proving in llms through large\-scale synthetic data\.arXiv preprint arXiv:2405\.14333\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p3.1),[Table 1](https://arxiv.org/html/2607.07779#S2.T1.3.3.3.3),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p1.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p3.1)\.
- DeepSeek\-AI \(2024b\)DeepSeek\-v3 technical report\.arXiv preprint arXiv:2412\.19437\.Cited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.28.1)\.
- DeepSeek\-AI \(2025\)DeepSeek\-r1: incentivizing reasoning capability in llms via reinforcement learning\.arXiv preprint arXiv:2501\.12948\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px3.p1.4),[§1](https://arxiv.org/html/2607.07779#S1.p2.1),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p4.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.10.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.29.1)\.
- A\. Didolkar, A\. Goyal, N\. R\. Ke, S\. Guo, M\. Valko, T\. Lillicrap, D\. Rezende, Y\. Bengio, M\. C\. Mozer, and S\. Arora \(2024\)Metacognitive capabilities of llms: an exploration in mathematical problem solving\.arXiv preprint arXiv:2405\.12205\.Cited by:[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p4.1)\.
- R\. Ding, C\. Zhang, L\. Wang, Y\. Xu, M\. Ma, W\. Zhang, S\. Qin, S\. Rajmohan, Q\. Lin, and D\. Zhang \(2024\)Everything of thoughts: defying the law of penrose triangle for thought generation\.arXiv preprint\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- DoD \(2007\)DARPA mathematical challenges\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.2.2.2.2.1.1)\.
- K\. Dong and T\. Ma \(2025\)STP: self\-play llm theorem provers with iterative conjecturing and proving\.arXiv preprint arXiv:2502\.00212\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.15.1),[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p1.1)\.
- K\. Dong, A\. Mahankali, and T\. Ma \(2024\)Formal theorem proving by rewarding llms to decompose proofs hierarchically\.arXiv preprint arXiv:2411\.01829\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p3.1)\.
- B\. Duan, X\. Liang, S\. Lu, Y\. Wang, Y\. Shen, K\. Chang, Y\. N\. Wu, M\. Yang, W\. Chen, and Y\. Gong \(2025\)Gold\-medal\-level olympiad geometry solving with efficient heuristic auxiliary constructions\.arXiv preprint arXiv:2512\.00097\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.SSS0.Px2.p1.1),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1)\.
- A\. Dubey, A\. Jauhri, A\. Pandey, A\. Kadian, A\. Al\-Dahle, A\. Letman, A\. Mathur, A\. Schelten, A\. Yang, A\. Fan,et al\.\(2024\)The llama 3 herd of models\.arXiv preprint arXiv:2407\.21783\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1)\.
- B\. Ekici, A\. Mebsout, C\. Tinelli, C\. Keller, G\. Katz, A\. Reynolds, and C\. Barrett \(2017\)SMTCoq: a plug\-in for integrating smt solvers into coq\.InInternational Conference on Computer Aided Verification,pp\. 126–133\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- P\. Erdős and R\. L\. Graham \(1999\)Old and new problems and results in combinatorial number theory\.Monographies de L’Enseignement Mathématique, Vol\.28,L’Enseignement Mathématique\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.5.5.5.3.1.1)\.
- P\. Erdős \(1957\)Some unsolved problems\.\.Michigan Mathematical Journal4\(3\),pp\. 291–300\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p4.1)\.
- T\. Feng, T\. Trinh, G\. Bingham, J\. Kang, S\. Zhang, S\. Kim, K\. Barreto, C\. Schildkraut, J\. Jung, J\. Seo, C\. Pagano, Y\. Chervonyi, D\. Hwang, K\. Hou, S\. Gukov, C\. Tsai, H\. Choi, Y\. Jin, W\. Li, H\. Wu, R\. Shiu, Y\. Shih, Q\. V\. Le, and T\. Luong \(2026a\)Semi\-autonomous mathematics discovery with Gemini: a case study on the Erdős problems\.arXiv preprint arXiv:2601\.22401\.Cited by:[§4\.3](https://arxiv.org/html/2607.07779#S4.SS3.p5.1)\.
- T\. Feng, T\. H\. Trinh, G\. Bingham,et al\.\(2026b\)Towards autonomous mathematics research\.arXiv preprintarXiv:2602\.10177\.Cited by:[§4\.3](https://arxiv.org/html/2607.07779#S4.SS3.p5.1),[Table 6](https://arxiv.org/html/2607.07779#S4.T6)\.
- E\. First, M\. N\. Rabe, T\. Ringer, and Y\. Brun \(2023\)Baldur: whole\-proof generation and repair with large language models\.arXiv preprint arXiv:2303\.04910\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- P\. Frankl and V\. Rödl \(1995\)Extremal problems on set systems\.Random Structures & Algorithms\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.6.6.6.2.1.1)\.
- S\. Frieder, L\. Pinchetti, R\. Griffiths, T\. Salvatori, T\. Lukasiewicz, P\. C\. Petersen, A\. Chevalier, and J\. Berner \(2023\)Mathematical capabilities of chatgpt\.NeurIPS\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- Y\. Fu, H\. Peng, A\. Sabharwal, P\. Clark, and T\. Khot \(2023\)Complexity\-based prompting for multi\-step reasoning\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- G\. Gao, Y\. Wang, J\. Jiang, Q\. Gao, Z\. Qin, T\. Xu, and B\. Dong \(2024\)Herald: a natural language annotated lean 4 dataset\.arXiv preprint arXiv:2410\.10878\.Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p3.1)\.
- J\. Gao, R\. Pi, J\. Lin, S\. Xu, Y\. Zheng, and T\. Zhang \(2025\)G\-llava: solving geometric problem with multi\-modal large language model\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- L\. Gao, A\. Madaan, S\. Zhou, U\. Alon, P\. Liu, Y\. Yang, J\. Callan, and G\. Neubig \(2023\)PAL: program\-aided language models\.ICML\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- Y\. Ge, D\. Yang, and A\. L\. Bertozzi \(2025\)Iterative active learning strategies for subgraph matching\.Pattern Recognition158,pp\. 110797\.External Links:ISSN 0031\-3203,[Document](https://dx.doi.org/https%3A//doi.org/10.1016/j.patcog.2024.110797),[Link](https://www.sciencedirect.com/science/article/pii/S003132032400548X)Cited by:[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p2.1)\.
- Gemini Team, R\. Anil, S\. Borgeaud, Y\. Wu, J\. Alayrac, J\. Yu, R\. Soricut, J\. Schalkwyk, A\. M\. Dai, A\. Hauth,et al\.\(2023\)Gemini: a family of highly capable multimodal models\.arXiv preprint arXiv:2312\.11805\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1)\.
- B\. Georgiev, J\. Gómez\-Serrano, T\. Tao, and A\. Z\. Wagner \(2025\)Mathematical exploration and discovery at scale\.arXiv preprint arXiv:2511\.02864\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p2.1)\.
- E\. Glazer, E\. Erdil, T\. Besiroglu, D\. Chicharro, E\. Chen, A\. Gunning, C\. F\. Olsson, J\. Denain, A\. Ho, E\. d\. O\. Santos,et al\.\(2024\)Frontiermath: a benchmark for evaluating advanced mathematical reasoning in ai\.arXiv preprint arXiv:2411\.04872\.Cited by:[§A\.1](https://arxiv.org/html/2607.07779#A1.SS1.p3.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1)\.
- F\. Gloeckle, J\. Limperg, G\. Synnaeve, and A\. Hayat \(2024\)Abel: sample efficient online reinforcement learning for neural theorem proving\.The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24\.Cited by:[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.22.1)\.
- G\. Gonthier, L\. Kovács,et al\.\(2013\)A machine\-checked proof of the odd order theorem\.International Conference on Interactive Theorem Proving\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- G\. Gonthier \(2008\)Formal proof–the four\-color theorem\.Notices of the AMS\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- Google DeepMind \(2025\)Advanced version of gemini with deep think officially achieves gold\-medal standard at the international mathematical olympiad\.Note:[https://goo\.gle/imo\-gold](https://goo.gle/imo-gold)Cited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.12.1.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.4.1.1)\.
- M\. J\. Gordon and T\. F\. Melham \(1993\)Introduction to hol: a theorem proving environment for higher order logic\.Cambridge University Press\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- Z\. Gou, Z\. Shao, Y\. Gong, Y\. Yang, M\. Huang, N\. Duan, and W\. Chen \(2024\)ToRA: a tool\-integrated reasoning agent for mathematical problem solving\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1),[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- M\. Gromov \(2017\)101 questions, problems and conjectures around scalar curvature\.Note:ManuscriptIncomplete and unedited versionCited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.13.13.24.1.1.1)\.
- A\. Grothendieck \(1969\)Standard conjectures on algebraic cycles\.Algebraic Geometry \(Bombay 1968\)\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.13.13.21.1.1.1)\.
- R\. Gruetzemacher and J\. Whittlestone \(2022\)The transformative potential of artificial intelligence\.Futures\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- C\. Gulcehre, T\. L\. Paine, S\. Srinivasan, M\. Kochenderfer, L\. Xiao, A\. Joshi, R\. Agarwal, D\. Moyer, Q\. Le, and D\. Zhou \(2023\)Reinforced self\-training \(rest\) for language modeling\.arXiv preprint\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- R\. K\. Guy \(2004\)Unsolved problems in number theory\.Springer Nature\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.3.3.3.2.1.1)\.
- T\. Hales, M\. Adams, G\. Bauer, D\. T\. Dang, J\. Harrison, T\. L\. Hoang, C\. Kaliszyk, V\. Magron, S\. McLaughlin, T\. T\. Nguyen, T\. Q\. Nguyen, T\. Nipkow, S\. Obua, J\. Pleso, J\. Rute, A\. Solovyev, A\. H\. T\. Ta, T\. N\. Tran, D\. T\. Trieu, J\. Urban, K\. K\. Vu, and R\. Zumkeller \(2017\)A formal proof of the kepler conjecture\.Forum of Mathematics, Pi\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- J\. M\. Han, J\. Rute, Y\. Wu, E\. W\. Ayers, and S\. Polu \(2021\)Proof artifact co\-training for theorem proving with language models\.arXiv preprint arXiv:2102\.06203\.Cited by:[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.27.1)\.
- S\. Hao, Y\. Gu, H\. Ma, J\. J\. Hong, Z\. Wang, D\. Z\. Wang, and Z\. Hu \(2023\)Reasoning with language model is planning with world model\.EMNLP\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- C\. He, R\. Luo, Y\. Bai, S\. Hu, Z\. L\. Thai, J\. Shen, J\. Hu, X\. Han, Y\. Huang, Y\. Zhang,et al\.\(2024\)OlympiadBench: a challenging benchmark for promoting agi with olympiad\-level bilingual multimodal scientific problems\.ACL\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- D\. Hendrycks, C\. Burns, S\. Basart, A\. Zou, M\. Mazeika, D\. Song, and J\. Steinhardt \(2021a\)Measuring massive multitask language understanding\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. Steinhardt \(2021b\)Measuring mathematical problem solving with the math dataset\.NeurIPS\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p2.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- D\. Hilbert \(1902\)Mathematical problems\.InBulletin of the American Mathematical Society,Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.1.1.1.2.1.1)\.
- J\. Hu, J\. Zhang, Y\. Zhao, and T\. Ringer \(2025a\)HybridProver: augmenting theorem proving with llm\-driven proof synthesis and refinement\.arXiv preprint arXiv:2505\.15740\.Cited by:[§B\.5](https://arxiv.org/html/2607.07779#A2.SS5.p4.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p4.1)\.
- J\. Hu, Y\. Zhang, S\. Shang, X\. Yang, Y\. Peng, Z\. Huang, H\. Zhou, X\. Wu, J\. Cheng, F\. Wan,et al\.\(2026\)PaCoRe: learning to scale test\-time compute with parallel coordinated reasoning\.arXiv preprint arXiv:2601\.05593\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p2.1)\.
- R\. Hu, S\. Lin, Y\. Xiu, and Y\. Liu \(2025b\)LTRAG: enhancing autoformalization and self\-refinement for logical reasoning with thought\-guided rag\.Findings of the Association for Computational Linguistics: ACL 2025\.Cited by:[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px1.p1.1),[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p2.1)\.
- C\. Huang, W\. Yu, X\. Wang, H\. Zhang, Z\. Li, R\. Li, J\. Huang, H\. Mi, and D\. Yu \(2025a\)R\-zero: self\-evolving reasoning llm from zero data\.arXiv preprint arXiv:2508\.05004\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- L\. Huang, W\. Yu, W\. Ma, W\. Zhong, Z\. Feng, H\. Wang, Q\. Chen, W\. Peng, X\. Feng, B\. Qin,et al\.\(2025b\)A survey on hallucination in large language models: principles, taxonomy, challenges, and open questions\.ACM Transactions on Information Systems43\(2\),pp\. 1–55\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p2.1)\.
- L\. Huang, W\. Yu, W\. Ma, W\. Zhong,et al\.\(2025c\)A survey on hallucination in large language models\.ACM Transactions on Information Systems\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom, O\. Bertolli, T\. Zahavy, A\. Mandhane, J\. Yung, I\. Beloshapka, B\. Ibarz, V\. Veeriah, L\. Yu, O\. Nash, P\. Lezeau, S\. Mercuri, C\. Sönne, B\. Mehta, A\. Davies, D\. Zheng, F\. Pedregosa, Y\. Li, I\. von Glehn, M\. Rowland, S\. Albanie, A\. Velingker, S\. Schmitt, E\. Lockhart, E\. Hughes, H\. Michalewski, N\. Sonnerat, D\. Hassabis, P\. Kohli, and D\. Silver \(2025\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature\.External Links:ISSN 1476\-4687,[Link](https://doi.org/10.1038/s41586-025-09833-y),[Document](https://dx.doi.org/10.1038/s41586-025-09833-y)Cited by:[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1)\.
- A\. Jaech, A\. Kalai, A\. Lerer, A\. Richardson, A\. El\-Kishky, A\. Low, A\. Helyar, A\. Madry, A\. Beutel, A\. Carney,et al\.\(2024\)OpenAI o1 system card\.arXiv preprint arXiv:2412\.16720\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p2.1),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p4.1)\.
- X\. Ji, Y\. Liu, Q\. Wang, J\. Zhang, Y\. Yue, R\. Shi, C\. Sun, F\. Zhang, G\. Zhou, and K\. Gai \(2025\)Leanabell\-prover\-v2: verifier\-integrated reasoning for formal theorem proving via reinforcement learning\.arXiv preprint arXiv:2507\.08649\.Cited by:[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.11.1)\.
- A\. Q\. Jiang, W\. Li, and M\. Jamnik \(2023a\)Multilingual mathematical autoformalization\.arXiv preprint arXiv:2311\.03755\.Cited by:[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p2.1)\.
- A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, W\. Li, J\. Liu, M\. Jamnik, T\. Lacroix, Y\. Wu, and G\. Lample \(2023b\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.International Conference on Learning Representations\.Cited by:[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px2.p1.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p3.1),[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p3.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- A\. Q\. Jiang, W\. Li, J\. M\. Han, and Y\. Wu \(2021\)LISA: language models of isabelle proofs\.In6th Conference on Artificial Intelligence and Theorem Proving,pp\. 378–392\.Cited by:[item ❸](https://arxiv.org/html/2607.07779#S2.I1.ix3.p1.1),[Table 2](https://arxiv.org/html/2607.07779#S2.T2.1.1.2.7)\.
- A\. Q\. Jiang, W\. Li, S\. Tworkowski, K\. Czechowski, T\. Odrzygóźdź, P\. Miloś, Y\. Wu, and M\. Jamnik \(2022\)Thor: wielding hammers to integrate language models and automated theorem provers\.arXiv preprint arXiv:2205\.10893\.Cited by:[§B\.2](https://arxiv.org/html/2607.07779#A2.SS2.SSS0.Px3.p1.1),[item ❸](https://arxiv.org/html/2607.07779#S2.I1.ix3.p1.1),[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p3.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p2.1)\.
- J\. Jiang, T\. Ding, and Z\. Zhu \(2026\)DeltaEvolve: accelerating scientific discovery through momentum\-driven evolution\.arXiv preprint arXiv:2602\.02919\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p2.1)\.
- J\. Jiang, W\. He, Y\. Wang, G\. Gao, Y\. Hu, J\. Wang, N\. Guan, P\. Wu, C\. Dai, L\. Xiao, and B\. Dong \(2025\)FATE: a formal benchmark series for frontier algebra of multiple difficulty levels\.External Links:arXiv 2511\.02872Cited by:[§A\.1](https://arxiv.org/html/2607.07779#A1.SS1.p3.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.10.1)\.
- S\. Kadavath, T\. Conerly, A\. Askell,et al\.\(2022\)Language models \(mostly\) know what they know\.arXiv preprint 2207\.05221\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- G\. E\. Karniadakis, I\. G\. Kevrekidis, L\. Lu, P\. Perdikaris, S\. Wang, and L\. Yang \(2021\)Physics\-informed machine learning\.Nature Reviews Physics3,pp\. 422–440\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- M\. Kaufmann and J\. S\. Moore \(1996\)ACL2: an industrial strength version of nqthm\.InProceedings of 11th Annual Conference on Computer Assurance\. COMPASS’96,pp\. 23–34\.Cited by:[item ❷](https://arxiv.org/html/2607.07779#S2.I1.ix2.p1.1)\.
- A\. E\. Kellison and A\. W\. Appel \(2022\)Verified numerical methods for ordinary differential equations\.InInternational Workshop on Numerical Software Verification,pp\. 147–163\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- T\. Kojima, S\. S\. Gu, M\. Reid, Y\. Matsuo, and Y\. Iwasawa \(2022\)Large language models are zero\-shot reasoners\.Advances in Neural Information Processing Systems\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- L\. Kovács and A\. Voronkov \(2013\)First\-order theorem proving and vampire\.InInternational Conference on Computer Aided Verification,Cited by:[item ❷](https://arxiv.org/html/2607.07779#S2.I1.ix2.p1.1),[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p4.1)\.
- L\. Kuhn, Y\. Gal, and S\. Farquhar \(2023\)Semantic uncertainty: linguistic invariances for uncertainty estimation in natural language generation\.ICLR\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- A\. Kumarappan, M\. Tiwari, P\. Song, R\. J\. George, C\. Xiao, and A\. Anandkumar \(2025\)LeanAgent: lifelong learning for formal theorem proving\.arXiv preprint arXiv:2410\.06209\.Cited by:[§B\.5](https://arxiv.org/html/2607.07779#A2.SS5.p3.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p3.1)\.
- I\. Lakatos \(1976\)Proofs and refutations: the logic of mathematical discovery\.Cambridge University Press\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p3.1)\.
- S\. Lamont, C\. Walder, A\. Dezfouli, P\. Montague, and M\. Norrish \(2025\)3D\-prover: diversity driven theorem proving with determinantal point processes\.NeurIPS\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.20.1)\.
- G\. Lample, M\. Lachaux, T\. Lavril, X\. Martinet, A\. Hayat, G\. Ebner, A\. Rodriguez, and T\. Lacroix \(2022\)HyperTree proof search for neural theorem proving\.Advances in Neural Information Processing Systems36,pp\. 26337–26349\.Cited by:[§B\.2](https://arxiv.org/html/2607.07779#A2.SS2.SSS0.Px2.p1.3),[§1](https://arxiv.org/html/2607.07779#S1.p1.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.23.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- E\. Landau \(1912\)Gelöste und ungelöste probleme aus der theorie der primzahlverteilung und der riemannschen zetafunktion\.\.Jahresbericht der Deutschen Mathematiker\-Vereinigung21,pp\. 208–228\.External Links:[Link](http://eudml.org/doc/145337)Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.13.13.18.1.1.1)\.
- R\. P\. Langlands \(1967\)Letter to andré weil\.Note:Foundational document of the Langlands ProgramCited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.13.13.23.1.1.1)\.
- D\. Lazard \(1983\)Gröbner bases, gaussian elimination and resolution of systems of algebraic equations\.InEuropean Conference on Computer Algebra,pp\. 146–156\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.SSS0.Px1.p1.1),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p1.1)\.
- Y\. LeCun, Y\. Bengio, and G\. Hinton \(2015\)Deep learning\.Nature521\(7553\),pp\. 436–444\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- J\. Lee and J\. Seo \(2026\)Lower bounds for multivariate independence polynomials and their generalisations\.arXiv preprint arXiv:2602\.02450\.Cited by:[§4\.3](https://arxiv.org/html/2607.07779#S4.SS3.p5.1)\.
- R\. Y\. Lewis and M\. W\. Roux \(2022\)A bi\-directional extensible interface between lean and mathematica\.InJournal of Automated Reasoning,Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p4.1)\.
- A\. Lewkowycz, A\. Andreassen, D\. Dohan, E\. Dyer, H\. Michalewski, V\. Ramasesh, A\. Slone, C\. Anil, I\. Schlag, T\. Gutman\-Solo,et al\.\(2022\)Solving quantitative reasoning problems with language models\.NeurIPS\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- J\. LI, E\. Beeching, L\. Tunstall, B\. Lipkin, R\. Soletskyi, S\. C\. Huang, K\. Rasul, L\. Yu, A\. Jiang, Z\. Shen, Z\. Qin, B\. Dong, L\. Zhou, Y\. Fleureau, G\. Lample, and S\. Polu \(2024\)NuminaMath\.Numina\.Note:[\[https://huggingface\.co/AI\-MO/NuminaMath\-CoT\]\(https://github\.com/project\-numina/aimo\-progress\-prize/blob/main/report/numina\_dataset\.pdf\)](https://arxiv.org/html/2607.07779v1/%5Bhttps://huggingface.co/AI-MO/NuminaMath-CoT%5D(https://github.com/project-numina/aimo-progress-prize/blob/main/report/numina_dataset.pdf))Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- W\. Li, L\. Yu, Y\. Wu, and L\. C\. Paulson \(2020\)IsarStep: a benchmark for high\-level mathematical reasoning\.arXiv preprint arXiv:2006\.09265\.Cited by:[item ❸](https://arxiv.org/html/2607.07779#S2.I1.ix3.p1.1),[Table 2](https://arxiv.org/html/2607.07779#S2.T2.1.1.2.7)\.
- Y\. Li, D\. Du, L\. Song, C\. Li, W\. Wang, T\. Yang, and H\. Mi \(2024a\)HunyuanProver: a scalable data synthesis framework and guided tree search for automated theorem proving\.arXiv preprint arXiv:2412\.20735\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.13.1)\.
- Z\. Li, Z\. Li, W\. Tang, X\. Zhang, Y\. Yao, X\. Si, F\. Yang, K\. Yang, and X\. Ma \(2025\)Proving olympiad inequalities by synergizing llms and symbolic reasoning\.The Thirteenth International Conference on Learning Representations\.Cited by:[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p4.1)\.
- Z\. Li, J\. Sun, L\. Murphy, Q\. Su, Z\. Li, X\. Zhang, K\. Yang, and X\. Si \(2024b\)A survey on deep learning for theorem proving\.arXiv preprint arXiv:2404\.09939\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- X\. Liang, Z\. Li, Y\. Gong, Y\. Wang, H\. Zhang, Y\. Shen, Y\. N\. Wu, and W\. Chen \(2025a\)Sws: self\-aware weakness\-driven problem synthesis in reinforcement learning for llm reasoning\.arXiv preprint arXiv:2506\.08989\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- X\. Liang, Z\. Li, Z\. Lin, E\. H\. Jiang, H\. Zhang, Y\. Shen, K\. Chang, Y\. N\. Wu, Y\. Gong, and W\. Chen \(2026\)Training llms for divide\-and\-conquer reasoning elevates test\-time scalability\.arXiv preprint arXiv:2602\.02477\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- X\. Liang, Z\. Li, Y\. Gong, Y\. Shen, Y\. N\. Wu, Z\. Guo, and W\. Chen \(2025b\)Beyond pass@ 1: self\-play with variational problem synthesis sustains rlvr\.arXiv preprint arXiv:2508\.14029\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- Z\. Liang, L\. Song, Y\. Li, T\. Yang, F\. Zhang, H\. Mi, and D\. Yu \(2025c\)MPS\-prover: advancing stepwise theorem proving by multi\-perspective search and data curation\.arXiv preprint arXiv:2505\.10962\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1)\.
- Z\. Liang, L\. Song, Y\. Li, T\. Yang, F\. Zhang, H\. Mi, and D\. Yu \(2025d\)Towards solving more challenging IMO problems via decoupled reasoning and proving\.CoRRabs/2507\.06804\.External Links:[Link](https://doi.org/10.48550/arXiv.2507.06804),[Document](https://dx.doi.org/10.48550/ARXIV.2507.06804),2507\.06804Cited by:[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p3.1)\.
- H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. Cobbe \(2024\)Let’s verify step by step\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- J\. Limperg and A\. H\. From \(2023\)Aesop: white\-box best\-first search for lean\.InProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs,pp\. 245–258\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p5.1)\.
- H\. Lin, Z\. Sun, S\. Welleck, and Y\. Yang \(2024\)Lean\-star: learning to interleave thinking and proving\.arXiv preprint arXiv:2407\.10040\.Cited by:[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.21.1)\.
- Y\. Lin, S\. Tang, B\. Lyu, J\. Wu, H\. Lin, K\. Yang, J\. Li, M\. Xia, D\. Chen, S\. Arora,et al\.\(2025a\)Goedel\-prover: a frontier model for open\-source automated theorem proving\.arXiv preprint arXiv:2502\.07640\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px1.p1.4),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p1.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.16.1)\.
- Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun,et al\.\(2025b\)Goedel\-prover\-v2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.arXiv preprint arXiv:2508\.03613\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1),[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p3.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.5.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p6.1)\.
- W\. Linget al\.\(2023\)Natural language to code generation with execution\-based verification\.arXiv preprint\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- Z\. Ling, Y\. Fang, X\. Li, Z\. Huang, M\. Lee, R\. Memisevic, and H\. Su \(2024\)Deductive verification of chain\-of\-thought reasoning\.NeurIPS\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- J\. Liu, X\. Lin, J\. Bayer, Y\. Dillies, W\. Jiang, X\. Liang, R\. Soletskyi, H\. Wang, Y\. Xie, B\. Xiong,et al\.\(2025a\)CombiBench: benchmarking llm capability for combinatorial mathematics\.arXiv preprint arXiv:2505\.03171\.Cited by:[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.6.1)\.
- J\. Liu, Z\. Zhou, Z\. Zhu, M\. D\. Santos, W\. He, J\. Liu, R\. Wang, Y\. Xie, J\. Zhao, Q\. Wang,et al\.\(2026\)Numina\-lean\-agent: an open and general agentic reasoning system for formal mathematics\.arXiv preprint arXiv:2601\.14027\.Cited by:[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p3.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- X\. Liu, K\. Bao, J\. Zhang, Y\. Liu, Y\. Chen, Y\. Liu, Y\. Jiao, and T\. Luo \(2025b\)ATLAS: autoformalizing theorems through lifting, augmentation, and synthesis of data\.arXiv preprint arXiv:2502\.05567\.Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p6.1)\.
- S\. M\. Loos, G\. Irving, C\. Szegedy, and C\. Kaliszyk \(2017\)Deep network guided proof search\.arXiv preprint arXiv:1701\.06972\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1)\.
- J\. Lu, Z\. Dou, H\. Wang, Z\. Cao, J\. Dai, Y\. Feng, and Z\. Guo \(2024a\)Autopsv: automated process\-supervised verifier\.Advances in Neural Information Processing Systems37,pp\. 79935–79962\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- J\. Lu, Y\. Wan, Y\. Huang, J\. Xiong, Z\. Liu, and Z\. Guo \(2024b\)Formalalign: automated alignment evaluation for autoformalization\.arXiv preprint arXiv:2410\.10135\.Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p2.1)\.
- J\. Lu, Y\. Wan, Z\. Liu, Y\. Huang, J\. Xiong, C\. Liu, J\. Shen, H\. Jin, J\. Zhang, H\. Wang,et al\.\(2024c\)Process\-driven autoformalization in lean 4\.arXiv preprint arXiv:2406\.01940\.Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p2.1)\.
- M\. Lu, B\. Delaware, and T\. Zhang \(2024d\)Proof automation with large language models\.Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering \(ASE 2024\)\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px1.p1.4),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p2.1)\.
- P\. Lu, H\. Bansal, T\. Xia, J\. Liu, C\. Li, H\. Hajishirzi, H\. Cheng, K\. Chang, M\. Galley, and J\. Gao \(2024e\)MathVista: evaluating mathematical reasoning of foundation models in visual contexts\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- P\. Lu, R\. Gong, S\. Jiang, L\. Qiu, S\. Huang, X\. Liang, and J\. Gao \(2021\)Inter\-gps: interpretable geometry problem solving with formal language and symbolic reasoning\.ACL\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- P\. Lu, J\. Sheng, L\. Lyu, J\. Jin, T\. Xia, A\. Gu, and J\. Zou \(2025\)Solving inequality proofs with large language models\.External Links:arXiv 2506\.07927Cited by:[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.9.1)\.
- H\. Luo, Q\. Sun, C\. Xu, P\. Zhao, J\. Lou, C\. Tao, X\. Geng, Q\. Lin, S\. Chen, and D\. Zhang \(2023\)WizardMath: empowering mathematical reasoning for large language models via reinforced evol\-instruct\.arXiv preprint\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- L\. Luo, Y\. Xu, B\. Lin, Y\. Liu, Y\. Ao, and J\. Fang \(2024\)Improve mathematical reasoning in language models by automated process supervision\.arXiv preprint\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- T\. Luong, D\. Hwang, H\. H\. Nguyen,et al\.\(2025\)Towards robust mathematical reasoning\.EMNLP\.Cited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.14.1)\.
- J\. Ma and Q\. Tang \(2026\)An Erdős problem on random subset sums in finite abelian groups\.arXiv preprint arXiv:2602\.05768\.Cited by:[§4\.3](https://arxiv.org/html/2607.07779#S4.SS3.p5.1)\.
- MAA \(2024\)American invitational mathematics examination \(AIME\)\.Mathematical Association of America \(MAA\)\.Note:Mathematics Competition SeriesExternal Links:[Link](https://maa.org/math-competitions/aime)Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p2.1)\.
- A\. Madaan, N\. Tandon, P\. Gupta, S\. Hallinan, L\. Gao, S\. Wiegreffe, U\. Alon, N\. Dziri, S\. Prabhumoye, Y\. Yang,et al\.\(2023\)Self\-refine: iterative refinement with self\-feedback\.NeurIPS\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- A\. Mahboubi and E\. Tassi \(2022\)Mathematical components\.Zenodo\.External Links:[Document](https://dx.doi.org/10.5281/zenodo.7118596),[Link](https://doi.org/10.5281/zenodo.7118596)Cited by:[§2\.2](https://arxiv.org/html/2607.07779#S2.SS2.p1.1)\.
- N\. McAleese, R\. Pokorny, J\. Uribe,et al\.\(2024\)LLM critics help catch llm bugs\.OpenAI Technical Report\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- L\. McGinness and P\. Baumgartner \(2024\)Automated theorem provers help improve large language model reasoning\.arXiv preprint arXiv:2410\.04492\.Cited by:[item ❸](https://arxiv.org/html/2607.07779#S2.I1.ix3.p1.1)\.
- C\. McLarty, J\. Gray, and K\. Parshall \(2007\)The rising sea: grothendieck on simplicity and generality\.Episodes in the history of modern algebra \(1800–1950\)32,pp\. 301–325\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p3.1)\.
- N\. D\. Megill and D\. A\. Wheeler \(2019\)Metamath: a computer language for pure mathematics\.Lulu Press\.Cited by:[item ❺](https://arxiv.org/html/2607.07779#S2.I1.ix5.p1.1)\.
- N\. Megill \(2007\)Metamath: a computer language for pure mathematics\.Lulu\. com\.Cited by:[item ❺](https://arxiv.org/html/2607.07779#S2.I1.ix5.p1.1)\.
- A\. Mohamed, T\. Mascarenhas, H\. Khan, H\. Barbosa, A\. Reynolds, Y\. Qian, C\. Tinelli, and C\. Barrett \(2025\)LEAN\-smt: an smt tactic for discharging proof goals in lean\.InInternational Conference on Computer Aided Verification,pp\. 197–212\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- H\. Moore and A\. Shah \(2025\)Evaluating autoformalization robustness via semantically similar paraphrasing\.arXiv preprint arXiv:2511\.12784\.Cited by:[§A\.3](https://arxiv.org/html/2607.07779#A1.SS3.p2.2)\.
- B\. Naskręcki and K\. Ono \(2025\)Mathematical discovery in the age of artificial intelligence\.Nature Physics\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p1.1)\.
- A\. Newell, J\. C\. Shaw, and H\. A\. Simon \(1956\)The logic theory machine: a complex information processing system\.IRE Transactions on Information Theory\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p2.1)\.
- A\. Novikov, N\. Vũ, M\. Eisenberger, E\. Dupont, P\. Huang, A\. Z\. Wagner, S\. Shirobokov, B\. Kozlovskii, F\. J\. Ruiz, A\. Mehrabian,et al\.\(2025\)AlphaEvolve: a coding agent for scientific and algorithmic discovery\.arXiv preprint arXiv:2506\.13131\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p2.1)\.
- OpenAI \(2024\)GPT\-4 system card\.Note:OpenAI Technical ReportCited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- OpenAI \(2025a\)GPT\-5 system card\.Note:OpenAI Technical ReportCited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.15.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.16.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.6.1)\.
- OpenAI \(2025b\)GPT\-5\.1 system card\.Note:OpenAI Technical ReportCited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.20.1)\.
- OpenAI \(2025c\)OpenAI o3 and o4\-mini system card\.Note:OpenAI Technical ReportCited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.23.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.24.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.9.1)\.
- OpenAI \(2025d\)OpenAI o3\-mini system card\.Note:[https://cdn\.openai\.com/o3\-mini\-system\-card\-feb10\.pdf](https://cdn.openai.com/o3-mini-system-card-feb10.pdf)Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p4.1)\.
- OpenAI \(2026\)Our first proof submissions\.Note:[https://openai\.com/index/first\-proof\-submissions/](https://openai.com/index/first-proof-submissions/)Accessed: 2026\-02\-25Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- A\. Ospanov, F\. Farnia, and R\. Yousefzadeh \(2025\)MiniF2F\-lean revisited: reviewing limitations and charting a path forward\.External Links:arXiv 2511\.03108Cited by:[§A\.1](https://arxiv.org/html/2607.07779#A1.SS1.p1.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p3.1)\.
- L\. Ouyang, J\. Wu, X\. Jiang, D\. Almeida, C\. Wainwright, P\. Mishkin, C\. Zhang, S\. Agarwal, K\. Slama, A\. Ray,et al\.\(2022\)Training language models to follow instructions with human feedback\.NeurIPS\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- S\. Owre, J\. M\. Rushby, and N\. Shankar \(1992\)PVS: a prototype verification system\.InInternational Conference on Automated Deduction,pp\. 748–752\.Cited by:[item ❹](https://arxiv.org/html/2607.07779#S2.I1.ix4.p1.1)\.
- A\. Paliwal, S\. M\. Loos, M\. N\. Rabe, K\. Bansal, and C\. Szegedy \(2019\)Graph representations for higher\-order logic and theorem proving\.arXiv preprint arXiv:1905\.10006\.Cited by:[§2\.7](https://arxiv.org/html/2607.07779#S2.SS7.p1.1)\.
- K\. Papineni, S\. Roukos, T\. Ward, and W\. Zhu \(2002\)Bleu: a method for automatic evaluation of machine translation\.InProceedings of the 40th annual meeting of the Association for Computational Linguistics,pp\. 311–318\.Cited by:[§A\.3](https://arxiv.org/html/2607.07779#A1.SS3.p2.2)\.
- L\. C\. Paulson and J\. C\. Blanchette \(2012\)Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers\.InIWIL,Cited by:[item ❸](https://arxiv.org/html/2607.07779#S2.I1.ix3.p1.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p2.1),[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p4.1)\.
- L\. C\. Paulson \(1994\)Isabelle: a generic theorem prover\.Springer Verlag\.Cited by:[item ❸](https://arxiv.org/html/2607.07779#S2.I1.ix3.p1.1),[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- S\. Polu, J\. M\. Han, K\. Zheng, M\. B\. Baksys, I\. Babuschkin, and I\. Sutskever \(2023\)Formal mathematics statement curriculum learning\.ICLR\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- S\. Polu and I\. Sutskever \(2020\)Generative language modeling for automated theorem proving\.arXiv preprint arXiv:2009\.03393\.Cited by:[item ❺](https://arxiv.org/html/2607.07779#S2.I1.ix5.p1.1),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p2.1),[Table 2](https://arxiv.org/html/2607.07779#S2.T2.1.1.5.7)\.
- D\. Quillen \(2006\)Higher algebraic k\-theory: i\.Springer\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.13.13.22.1.1.1)\.
- M\. Raissi, P\. Perdikaris, and G\. E\. Karniadakis \(2019\)Physics\-informed neural networks: a deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations\.Journal of Computational Physics\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- M\. Reid, N\. Savinov, D\. Teplyashin, D\. Lepikhin, T\. Lillicrap, J\. Alayrac, R\. Soricut, A\. Lazaridou, O\. Firat, J\. Schrittwieser,et al\.\(2024\)Gemini 1\.5: unlocking multimodal understanding across millions of tokens of context\.arXiv preprint arXiv:2403\.05530\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1)\.
- Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang,et al\.\(2025\)DeepSeek\-prover\-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.arXiv preprint arXiv:2504\.21801\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px2.p1.3),[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px2.p1.1),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1),[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p3.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.5.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.7.1),[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p3.1)\.
- J\. A\. Robinson \(1965\)A machine\-oriented logic based on the resolution principle\.Journal of the ACM\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p3.1)\.
- M\. Rossel \(2024\)Lean\-egg: e\-graph integration for the lean theorem prover\.Note:[https://github\.com/marcusrossel/lean\-egg](https://github.com/marcusrossel/lean-egg)Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p3.1)\.
- T\. Schick, J\. Dwivedi\-Yu, R\. Dessì, R\. Raileanu, M\. Lomeli, E\. Hambro, L\. Zettlemoyer, N\. Cancedda, and T\. Scialom \(2023\)Toolformer: language models can teach themselves to use tools\.Advances in Neural Information Processing Systems36,pp\. 68539–68551\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- J\. Schulman, F\. Wolski, P\. Dhariwal, A\. Radford, and O\. Klimov \(2017\)Proximal policy optimization algorithms\.arXiv preprint arXiv:1707\.06347\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px3.p1.4)\.
- S\. Schulz, S\. Cruanes, and P\. Vukmirović \(2019\)Faster, higher, stronger: e 2\.3\.InInternational Conference on Automated Deduction,pp\. 495–507\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p4.1)\.
- S\. Schulz \(2002\)E–a brainiac theorem prover\.Ai Communications15\(2\-3\),pp\. 111–126\.Cited by:[item ❷](https://arxiv.org/html/2607.07779#S2.I1.ix2.p1.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1)\.
- H\. Schurr, M\. Fleury, H\. Barbosa, and P\. Fontaine \(2021\)Alethe: towards a generic smt proof format\.InSeventh Workshop on Proof eXchange for Theorem Proving,Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p2.1)\.
- S\. Shang, R\. Wan, Y\. Peng, Y\. Wu, X\. Chen, J\. Yan, and X\. Zhang \(2025\)StepFun\-prover preview: let’s think and verify step by step\.arXiv preprint arXiv:2507\.20199\.Cited by:[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1)\.
- Z\. Shao, P\. Wang, Q\. Zhu, R\. Xu, J\. Song, X\. Bi, H\. Zhang, M\. Zhang, Y\. Li, Y\. Wu,et al\.\(2024\)Deepseekmath: pushing the limits of mathematical reasoning in open language models\.arXiv preprint arXiv:2402\.03300\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p3.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- W\. Shi, Z\. Hu, Y\. Bin, J\. Liu, Y\. Yang, S\. Ng, L\. Bing, and R\. K\. Lee \(2024\)Math\-llava: bootstrapping mathematical reasoning for multimodal large language models\.EMNLP Findings\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- N\. Shinn, F\. Cassano, A\. Gopinath, K\. R\. Narasimhan, and S\. Yao \(2023\)Reflexion: language agents with verbal reinforcement learning\.Advances in Neural Information Processing Systems37\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- D\. Silver, J\. Schrittwieser, K\. Simonyan, I\. Antonoglou, A\. Huang, A\. Guez, T\. Hubert, L\. Baker, M\. Lai, A\. Bolton,et al\.\(2017\)Mastering the game of go without human knowledge\.Nature550\(7676\),pp\. 354–359\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1)\.
- B\. Simon \(2000\)Schrödinger operators in the twenty\-first century\.Mathematical Physics 2000,pp\. 283–288\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.13.13.13.3.1.1)\.
- A\. Singh, J\. D\. Co\-Reyes, R\. Agarwal, A\. Anand, P\. Patil, P\. J\. Liu, J\. Harrison, J\. Lee, K\. Xu, A\. Parisi,et al\.\(2024\)Beyond human data: scaling self\-training for problem\-solving with language models\.TMLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- S\. Sinha, A\. Prabhu, P\. Kumaraguru, S\. Bhat, and M\. Bethge \(2024\)Wu’s method can boost symbolic ai to rival silver medalists and alphageometry to outperform gold medalists at imo geometry\.arXiv preprint arXiv:2404\.06405\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1)\.
- S\. Smale \(1998\)Mathematical problems for the next century\.The Mathematical Intelligencer20\(2\),pp\. 7–15\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.10.10.10.3.1.1)\.
- C\. Song, Z\. Wang, F\. Pu, H\. Wang, X\. Lin, J\. Liu, J\. Li, and Z\. Liu \(2025\)LeanGeo: formalizing competitional geometry problems in lean\.arXiv preprint arXiv:2508\.14644\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p5.1)\.
- P\. Song, K\. Yang, and A\. Anandkumar \(2024\)Towards a copilot for lean\.NeurIPS 2023 Workshop on MATH\-AI\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- D\. R\. Stoutemyer \(2014\)Ten commandments for good default expression simplification\.Journal of Symbolic Computation63,pp\. 93–117\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p2.1)\.
- T\. Tao \(2024a\)A mathematical proof assistant \(version 2\.0\)\.Note:[https://github\.com/teorth/estimates](https://github.com/teorth/estimates)Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p4.1)\.
- T\. Tao \(2024b\)Machine assisted proof\.Notices of the American Mathematical Society\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- R\. Tate, M\. Stepp, Z\. Tatlock, and S\. Lerner \(2009\)Equality saturation: a new approach to optimization\.InProceedings of the 36th ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages,pp\. 264–276\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p3.1)\.
- T\. C\. D\. Team \(2013\)The coq proof assistant reference manual\.Technical Report\.Cited by:[item ❶](https://arxiv.org/html/2607.07779#S2.I1.ix1.p1.1),[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- A\. Thakur, G\. Tsoukalas, Y\. Wen, J\. Xin, and S\. Chaudhuri \(2024\)An in\-context learning agent for formal theorem\-proving\.InFirst Conference on Language Modeling,Cited by:[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p3.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.26.1)\.
- The mathlib Community \(2020\)The lean mathematical library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,pp\. 367–381\.Cited by:[§2\.2](https://arxiv.org/html/2607.07779#S2.SS2.p1.1),[§2\.7](https://arxiv.org/html/2607.07779#S2.SS7.p1.1)\.
- N\. Thuerey, B\. Holzschuh, P\. Holl, G\. Kohl, M\. Lino,et al\.\(2025\)Physics\-based deep learning\.arXiv preprint arXiv:2109\.05237\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- W\. P\. Thurston \(1982\)Three\-dimensional manifolds, kleinian groups and hyperbolic geometry\.Bulletin of the American Mathematical Society\.Cited by:[Table 7](https://arxiv.org/html/2607.07779#S4.T7.8.8.8.2.1.1)\.
- S\. Toshniwal, I\. Moshkov, S\. Narenthiran, D\. Gitman, F\. Jia, and I\. Gitman \(2024\)OpenMathInstruct\-1: a 1\.8 million math instruction tuning dataset\.arXiv preprint arXiv:2402\.10176\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- H\. Touvron, L\. Martin, K\. Stone, P\. Albert, A\. Almahairi, Y\. Babaei, N\. Bashlykov, S\. Batra, P\. Bhargava, S\. Bhosale,et al\.\(2023\)Llama 2: open foundation and fine\-tuned chat models\.arXiv preprint arXiv:2307\.09288\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1)\.
- T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. Luong \(2024\)Solving olympiad geometry without human demonstrations\.Nature625,pp\. 476–482\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.SSS0.Px2.p1.1),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p1.1),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1),[item ❻](https://arxiv.org/html/2607.07779#S2.I1.ix6.p1.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- A\. Trybulec \(1993\)Some features of the mizar language\.Ina workshop in Turin, Italy,Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p6.1)\.
- G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. Chaudhuri \(2024\)PutnamBench: evaluating neural theorem\-provers on the putnam mathematical competition\.InThe Thirty\-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track,Cited by:[§A\.1](https://arxiv.org/html/2607.07779#A1.SS1.p2.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.4.1)\.
- J\. Uesato, N\. Kushman, R\. Kumar, F\. Song, N\. Siegel, L\. Wang, A\. Creswell, G\. Irving, and I\. Higgins \(2022\)Solving math word problems with process\- and outcome\-based feedback\.arXiv preprint arXiv:2211\.14275\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- F\. van Doorn, G\. Ebner, and R\. Y\. Lewis \(2020\)Maintaining a library of formal mathematics\.InInternational Conference on Intelligent Computer Mathematics,pp\. 251–267\.Cited by:[§2\.2](https://arxiv.org/html/2607.07779#S2.SS2.p1.1)\.
- S\. Varambally, T\. Voice, Y\. Sun, Z\. Chen, R\. Yu, and K\. Ye \(2025\)Hilbert: recursively building formal proofs with informal reasoning\.arXiv preprint arXiv:2509\.22819\.Cited by:[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p3.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.2.1)\.
- H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. D\. Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu,et al\.\(2025a\)Kimina\-prover preview: towards large formal reasoning models with reinforcement learning\.arXiv preprint arXiv:2504\.11354\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px3.p1.3),[§B\.5](https://arxiv.org/html/2607.07779#A2.SS5.p2.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p1.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.10.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.6.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p3.1)\.
- H\. Wang, H\. Xin, Z\. Liu, W\. Li, Y\. Huang, J\. Lu, Y\. Zhicheng, J\. Tang, J\. Yin, Z\. Li,et al\.\(2024a\)Proving theorems recursively\.Advances in Neural Information Processing Systems38\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1)\.
- H\. Wang, H\. Xin, C\. Zheng, Z\. Liu, Q\. Cao, Y\. Huang, J\. Xiong, H\. Shi, E\. Xie, J\. Yin,et al\.\(2024b\)LEGO\-prover: neural theorem proving with growing libraries\.InThe Twelfth International Conference on Learning Representations,Cited by:[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p3.1)\.
- H\. Wang, T\. Fu, Y\. Du, W\. Gao, K\. Huang, Z\. Liu, P\. Chandak, S\. Liu, P\. Van Katwyk, A\. Deac,et al\.\(2023a\)Scientific discovery in the age of artificial intelligence\.Nature620\(7972\),pp\. 47–60\.Cited by:[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p2.1)\.
- K\. Wang, H\. Ren, A\. Zhou, Z\. Lu, S\. Luo, W\. Shi, R\. Zhang, L\. Song, M\. Zhan, and H\. Li \(2024c\)MathCoder: seamless code integration in llms for enhanced mathematical reasoning\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- L\. Wang, W\. Xu, Y\. Lan, Z\. Hu, Y\. Lan, R\. K\. Lee, and E\. Lim \(2023b\)Plan\-and\-solve prompting: improving zero\-shot chain\-of\-thought reasoning by large language models\.ACL\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- M\. Wang and J\. Deng \(2020\)Learning to prove theorems by learning to generate theorems\.Advances in neural information processing systems33,pp\. 18146–18157\.Cited by:[item ❺](https://arxiv.org/html/2607.07779#S2.I1.ix5.p1.1)\.
- P\. Wang, L\. Li, Z\. Shao, R\. X\. Xu, D\. Dai, Y\. Li, D\. Chen, Y\. Wu, and Z\. Sui \(2024d\)Math\-shepherd: verify and reinforce llms step\-by\-step without human annotations\.ACL\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- R\. Wang, J\. Zhang, Y\. Jia, R\. Pan, S\. Diao, R\. Pi, and T\. Zhang \(2024e\)TheoremLlama: transforming general\-purpose llms into lean4 experts\.arXiv preprint arXiv:2407\.03203\.Cited by:[item ❶](https://arxiv.org/html/2607.07779#S2.I1.ix1.p1.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p1.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.24.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.25.1)\.
- X\. Wang, J\. Wei, D\. Schuurmans, Q\. Le, E\. Chi, S\. Narang, A\. Chowdhery, and D\. Zhou \(2023c\)Self\-consistency improves chain of thought reasoning in language models\.InProceedings of the International Conference on Learning Representations \(ICLR\),Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- Y\. Wang, S\. Su, Z\. Zeng, E\. Xu, L\. Ren, X\. Yang, Z\. Huang, X\. He, L\. Ma, B\. Peng,et al\.\(2025b\)Thetaevolve: test\-time learning on open problems\.arXiv preprint arXiv:2511\.23473\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p2.1)\.
- Z\. Wang, Y\. Chen, Z\. Li, Y\. Zhang, and Z\. Liu \(2025c\)QDTSynth: quality\-driven formal theorem synthesis towards boosting llms’ proving performance\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics,Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p6.1)\.
- C\. Wei, M\. Sun, and W\. Wang \(2024\)Proving olympiad algebraic inequalities without human demonstrations\.InAdvances in Neural Information Processing Systems,Vol\.37,pp\. 82811–82822\.Cited by:[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p4.1)\.
- J\. Wei, X\. Wang, Q\. Liu, B\. Yang, X\. Dong, H\. Huang, and W\. Wang \(2022\)Chain\-of\-thought prompting elicits reasoning in large language models\.arXiv preprint arXiv:2201\.11903\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1)\.
- C\. Weidenbach, R\. A\. Schmidt, T\. Hillenbrand, R\. Rusev, and D\. Topic \(2007\)System description: spass version 3\.0\.InInternational Conference on Automated Deduction,pp\. 514–520\.Cited by:[§2\.1](https://arxiv.org/html/2607.07779#S2.SS1.p4.1)\.
- S\. Welleck and R\. Saha \(2024\)LLMStep: llm proofstep suggestions in lean\.NeurIPS 2023 Workshop on MATH\-AI\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- X\. Wen, Z\. Liu, S\. Zheng, S\. Ye, Z\. Wu, Y\. Wang, Z\. Xu, X\. Liang, J\. Li, Z\. Miao,et al\.\(2025\)Reinforcement learning with verifiable rewards implicitly incentivizes correct reasoning in base llms\.arXiv preprint arXiv:2506\.14245\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- K\. Weng, L\. Du, S\. Li, W\. Lu, H\. Sun, H\. Liu, and T\. Zhang \(2025\)Autoformalization in the era of large language models: A survey\.arXiv preprint arXiv:2505\.23486\.Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p2.1),[§5\.1](https://arxiv.org/html/2607.07779#S5.SS1.p1.1)\.
- Y\. Weng, M\. Zhu, F\. Xia, B\. Li, S\. He, S\. Liu, B\. Sun, K\. Liu, and J\. Zhao \(2023\)Large language models are better reasoners with self\-verification\.InFindings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6\-10, 2023,Findings of ACL, Vol\.EMNLP 2023,pp\. 2550–2575\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- M\. J\. Wester \(1999\)A critique of the mathematical abilities of ca systems\.InComputer Algebra Systems: A Practical Guide,pp\. 436\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p2.1)\.
- D\. Whalen \(2016\)Holophrasm: a neural automated theorem prover for higher\-order logic\.arXiv preprint arXiv:1608\.02644\.Cited by:[item ❺](https://arxiv.org/html/2607.07779#S2.I1.ix5.p1.1)\.
- M\. Willsey, C\. Nandi, Y\. R\. Wang, O\. Flatt, Z\. Tatlock, and P\. Panchekha \(2021\)Egg: fast and extensible equality saturation\.Proceedings of the ACM on Programming Languages5\(POPL\),pp\. 1–29\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p3.1)\.
- N\. Wischermann, C\. M\. Verdun, G\. Poesia, and F\. Noseda \(2025\)Proofcompass: enhancing specialized provers with llm guidance\.arXiv preprint arXiv:2507\.14335\.Cited by:[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1)\.
- D\. P\. Woodruff, V\. Cohen\-Addad, L\. Jain, J\. Mao, S\. Zuo, M\. Bateni, S\. Branzei, M\. P\. Brenner, L\. Chen, Y\. Feng, L\. Fortnow, G\. Fu, Z\. Guan, Z\. Hadizadeh, M\. T\. Hajiaghayi, M\. JafariRaviz, A\. Javanmard, K\. Kawarabayashi, R\. Kumar, S\. Lattanzi, E\. Lee, Y\. Li, I\. Panageas, D\. Paparas, B\. Przybocki, B\. Subercaseaux, O\. Svensson, S\. Taherijam, X\. Wu, E\. Yogev, M\. Zadimoghaddam, S\. Zhou, Y\. Matias, J\. Manyika, and V\. Mirrokni \(2026\)Accelerating scientific research with Gemini: case studies and common techniques\.arXiv preprint arXiv:2602\.03837\.Cited by:[§4\.3](https://arxiv.org/html/2607.07779#S4.SS3.p5.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- M\. Wu, M\. Norrish, C\. Walder, and A\. Dezfouli \(2021\)TacticZero: learning to prove theorems from scratch with deep reinforcement learning\.Advances in Neural Information Processing Systems34,pp\. 9330–9342\.Cited by:[§2\.6](https://arxiv.org/html/2607.07779#S2.SS6.p3.1)\.
- S\. Wu, S\. Lu, Y\. Gong, N\. Duan, and P\. Wei \(2025\)Alchemy: amplifying theorem\-proving capability through symbolic mutation\.InThe Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24\-28, 2025,External Links:[Link](https://openreview.net/forum?id=7NL74jUiMg)Cited by:[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p1.1)\.
- T\. Wu, M\. Terry, and C\. J\. Cai \(2022a\)AI chains: transparent and controllable human\-ai interaction by chaining large language model prompts\.InProceedings of the 2022 CHI Conference on Human Factors in Computing Systems,CHI ’22\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- W\. Wu \(2008\)On the decision problem and the mechanization of theorem\-proving in elementary geometry\.World Scientific\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.SSS0.Px1.p1.1),[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p1.1),[item ❻](https://arxiv.org/html/2607.07779#S2.I1.ix6.p1.1)\.
- Y\. Wu, F\. Jia, S\. Zhang,et al\.\(2023\)An empirical study on challenging math problem solving with gpt\-4\.ICLR 2024 Workshop on LLM Agent\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy \(2022b\)Autoformalization with large language models\.Advances in Neural Information Processing Systems35,pp\. 32353–32368\.Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- Z\. Wu, S\. Huang, Z\. Zhou, H\. Ying, J\. Wang, D\. Lin, and K\. Chen \(2024a\)InternLM2\.5\-stepprover: advancing automated theorem proving via expert iteration on large\-scale lean problems\.arXiv preprint arXiv:2410\.15700\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px1.p1.4),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.14.1)\.
- Z\. Wu, J\. Wang, D\. Lin, and K\. Chen \(2024b\)Lean\-github: compiling github lean repositories for a versatile lean prover\.arXiv preprint arXiv:2407\.17227\.Cited by:[Table 1](https://arxiv.org/html/2607.07779#S2.T1.1.1.1.3),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.19.1)\.
- xAI \(2025a\)Grok 4 system card\.Note:xAI Technical ReportCited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.19.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.21.1),[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.8.1)\.
- xAI \(2025b\)Grok 4\.1 system card\.Note:xAI Technical ReportCited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.18.1)\.
- H\. Xin, D\. Guo, Z\. Shao, Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. Liang \(2024a\)DeepSeek\-prover: advancing theorem proving in llms through large\-scale synthetic data\.arXiv preprint arXiv:2405\.14333\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px2.p1.3),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1)\.
- H\. Xin, Z\. Z\. Ren, J\. Song, Z\. Shao, W\. Zhao, H\. Wang, B\. Liu, L\. Zhang, X\. Lu, Q\. Du, W\. Gao, Q\. Zhu, D\. Yang, Z\. Gou, Z\. F\. Wu, F\. Luo, and C\. Ruan \(2024b\)DeepSeek\-prover\-v1\.5: harnessing proof assistant feedback for reinforcement learning and monte\-carlo tree search\.arXiv preprint arXiv:2408\.08152\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px2.p1.3),[§B\.2](https://arxiv.org/html/2607.07779#A2.SS2.SSS0.Px2.p1.3),[§1](https://arxiv.org/html/2607.07779#S1.p3.1),[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p5.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.17.1)\.
- R\. Xin, Z\. Zheng, Y\. Nie, K\. Yuan, and X\. Xiao \(2025a\)Scaling up multi\-turn off\-policy rl and multi\-agent tree search for llm step\-provers\.arXiv preprint arXiv:2509\.06493\.Cited by:[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1)\.
- R\. Xin, C\. Xi, J\. Yang, F\. Chen, H\. Wu, X\. Xiao, Y\. Sun, S\. Zheng, and K\. Shen \(2025b\)BFS\-prover: scalable best\-first tree search for llm\-based automatic theorem proving\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\), ACL 2025, Vienna, Austria, July 27 \- August 1, 2025,pp\. 32588–32599\.Cited by:[§B\.2](https://arxiv.org/html/2607.07779#A2.SS2.SSS0.Px1.p1.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.12.1)\.
- A\. Yang, A\. Li, B\. Yang,et al\.\(2025a\)Qwen3 technical report\.arXiv preprint arXiv:2505\.09388\.Cited by:[Table 5](https://arxiv.org/html/2607.07779#S4.T5.1.1.30.1)\.
- A\. Yang, B\. Yang, B\. Zhang, B\. Hui, B\. Zheng, B\. Yu, C\. Li, D\. Liu, F\. Huang, H\. Wei,et al\.\(2024a\)Qwen2\.5 technical report\.arXiv preprint arXiv:2412\.15115\.Cited by:[§2\.3](https://arxiv.org/html/2607.07779#S2.SS3.p2.1)\.
- A\. Yang, B\. Zhang, B\. Hui, B\. Gao, B\. Yu, C\. Li, D\. Liu, J\. Tu, J\. Zhou, J\. Lin,et al\.\(2024b\)Qwen2\.5\-math technical report: toward mathematical expert model via self\-improvement\.arXiv preprint arXiv:2409\.12122\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- D\. Yang, Y\. Ge, T\. Nguyen, D\. Molitor, J\. D\. Moorman, and A\. L\. Bertozzi \(2023a\)Structural equivalence in subgraph matching\.IEEE Transactions on Network Science and Engineering10\(4\),pp\. 1846–1862\.External Links:[Document](https://dx.doi.org/10.1109/TNSE.2023.3236028)Cited by:[§5\.2](https://arxiv.org/html/2607.07779#S5.SS2.p2.1)\.
- K\. Yang and J\. Deng \(2019\)Learning to prove theorems via interacting with proof assistants\.InInternational Conference on Machine Learning,pp\. 6984–6994\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p1.1),[item ❶](https://arxiv.org/html/2607.07779#S2.I1.ix1.p1.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p2.1),[Table 2](https://arxiv.org/html/2607.07779#S2.T2.1.1.3.7),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p2.1)\.
- K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar \(2023b\)LeanDojo: theorem proving with retrieval\-augmented language models\.Advances in Neural Information Processing Systems36,pp\. 21573–21612\.Cited by:[item ❶](https://arxiv.org/html/2607.07779#S2.I1.ix1.p1.1),[§2\.7](https://arxiv.org/html/2607.07779#S2.SS7.p1.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p2.1),[Table 1](https://arxiv.org/html/2607.07779#S2.T1.2.2.2.3),[Table 2](https://arxiv.org/html/2607.07779#S2.T2.1.1.6.7),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p3.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.28.1),[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p2.1)\.
- T\. Yang, M\. Yan, H\. Zhao, and T\. Yang \(2025b\)LemmaHead: rag assisted proof generation using large language models\.arXiv preprint arXiv:2501\.15797\.Cited by:[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px1.p1.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p2.1)\.
- S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. L\. Griffiths, Y\. Cao, and K\. R\. Narasimhan \(2023\)Tree of thoughts: deliberate problem solving with large language models\.InAdvances in Neural Information Processing Systems,Vol\.37\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- S\. Yao, J\. Zhao, D\. Yu, N\. Du, I\. Shafran, K\. R\. Narasimhan, and Y\. Cao \(2022\)React: synergizing reasoning and acting in language models\.InThe eleventh international conference on learning representations,Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- H\. Ying, Z\. Wu, Y\. Geng, J\. Wang, D\. Lin, and K\. Chen \(2024a\)Lean workbook: a large\-scale lean problem set formalized from natural language math problems\.Advances in Neural Information Processing Systems37,pp\. 105848–105863\.Cited by:[§2\.7](https://arxiv.org/html/2607.07779#S2.SS7.p1.1)\.
- H\. Ying, S\. Zhang, L\. Li, Z\. Zhou, Y\. Shao, Z\. Fei, Y\. Ma, J\. Hong, K\. Liu, Z\. Wang,et al\.\(2024b\)InternLM\-math: open math large language models toward verifiable reasoning\.arXiv preprint arXiv:2402\.06332\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- R\. Yousefzadeh, X\. Cao, and A\. Ospanov \(2025\)A lean dataset for international math olympiad: small steps towards writing math proofs for hard problems\.Transactions on Machine Learning Research\.Cited by:[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1)\.
- D\. Yu, B\. Yang, D\. Liu, H\. Wang, and S\. Pan \(2023\)A survey on neural\-symbolic learning systems\.Neural Networks166,pp\. 105–126\.Cited by:[§1](https://arxiv.org/html/2607.07779#S1.p1.1)\.
- L\. Yu, W\. Jiang, H\. Shi, J\. Yu, Z\. Liu, Y\. Zhang, J\. T\. Kwok, Z\. Li, A\. Weller, and W\. Liu \(2024\)MetaMath: bootstrap your own mathematical questions for large language models\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- Q\. Yu, Z\. Zhang, R\. Zhu, Y\. Yuan, X\. Zuo, Y\. Yue, W\. Dai, T\. Fan, G\. Liu, L\. Liu,et al\.\(2025a\)DAPO: an open\-source llm reinforcement learning system at scale\.arXiv preprint arXiv:2503\.14476\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- Y\. Yu, Y\. Zhang, D\. Zhang, X\. Liang, H\. Zhang, X\. Zhang, M\. Khademi, H\. H\. Awadalla, J\. Wang, Y\. Yang,et al\.\(2025b\)Chain\-of\-reasoning: towards unified mathematical reasoning in large language models via a multi\-paradigm perspective\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 24914–24937\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- Z\. Yu, R\. Peng, K\. Ding, Y\. Li, Z\. Peng, M\. Liu, Y\. Zhang, Z\. Yuan, H\. Xin, W\. Huang,et al\.\(2025c\)FormalMath: benchmarking formal mathematical reasoning of large language models\.arXiv preprint arXiv:2505\.02735\.Cited by:[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 1](https://arxiv.org/html/2607.07779#S2.T1.7.7.7.3),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.7.1)\.
- Z\. Yuan, H\. Yuan, C\. Li, G\. Dong, K\. Lu, C\. Tan, C\. Zhou, and J\. Zhou \(2023\)Scaling relationship on learning mathematical reasoning with large language models\.arXiv preprint arXiv:2308\.01825\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- Y\. Yue, Y\. Yuan, Q\. Yu, X\. Zuo, R\. Zhu, W\. Xu, J\. Chen, C\. Wang, T\. Fan, Z\. Du,et al\.\(2025\)Vapo: efficient and reliable reinforcement learning for advanced reasoning tasks\.arXiv preprint arXiv:2504\.05118\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- M\. Yuksekgonul, D\. Koceja, X\. Li, F\. Bianchi, J\. McCaleb, X\. Wang, J\. Kautz, Y\. Choi, J\. Zou, C\. Guestrin,et al\.\(2026\)Learning to discover at test time\.Cited by:[§5\.3](https://arxiv.org/html/2607.07779#S5.SS3.p2.1)\.
- E\. Zelikman, Y\. Wu, J\. Mu, and N\. Goodman \(2022\)STaR: bootstrapping reasoning with reasoning\.Advances in Neural Information Processing Systems35,pp\. 15476–15488\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1),[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- Z\. Zeng, Y\. Liu, Y\. Wan, J\. Li, P\. Chen, J\. Dai, Y\. Yao, R\. Xu, Z\. Qi, W\. Zhao,et al\.\(2024\)Mr\-ben: a meta\-reasoning benchmark for evaluating system\-2 thinking in llms\.Advances in Neural Information Processing Systems37,pp\. 119466–119546\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p5.1)\.
- C\. Zhang, K\. M\. Collins, A\. Weller, and J\. B\. Tenenbaum \(2024a\)AI for mathematics: a cognitive science perspective\.NeurIPS 2023 Workshop on MATH\-AI\.Cited by:[§5\.5](https://arxiv.org/html/2607.07779#S5.SS5.p3.1)\.
- C\. Zhang, J\. Song, S\. Li, Y\. Liang, Y\. Ma, W\. Wang, Y\. Zhu, and S\. Zhu \(2026\)Proposing and solving olympiad geometry with guided tree search\.Nature Machine Intelligence,pp\. 1–12\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1),[§1](https://arxiv.org/html/2607.07779#S1.p3.1)\.
- J\. Zhang, Q\. Wang, X\. Ji, Y\. Liu, Y\. Yue, F\. Zhang, D\. Zhang, G\. Zhou, and K\. Gai \(2025a\)Leanabell\-prover: posttraining scaling in formal reasoning\.arXiv preprint arXiv:2504\.06122\.Cited by:[§B\.1](https://arxiv.org/html/2607.07779#A2.SS1.SSS0.Px2.p1.3),[§3\.1\.1](https://arxiv.org/html/2607.07779#S3.SS1.SSS1.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.18.1)\.
- L\. Zhang, M\. Valentino, and A\. Freitas \(2025b\)MASA: llm\-driven multi\-agent systems for autoformalization\.arXiv preprint arXiv:2510\.08988\.Cited by:[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px3.p1.1),[§2\.5](https://arxiv.org/html/2607.07779#S2.SS5.p1.1),[§3\.3](https://arxiv.org/html/2607.07779#S3.SS3.p3.1)\.
- R\. Zhang, D\. Jiang, Y\. Zhang, H\. Lin, Z\. Guo, P\. Qiu, A\. Zhou, P\. Lu, K\. Chang, Y\. Qiao,et al\.\(2024b\)Mathverse: does your multi\-modal llm truly see the diagrams in visual math problems?\.InEuropean Conference on Computer Vision,pp\. 169–186\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p6.1)\.
- Z\. Zhang, A\. Zhang, M\. Li, and A\. Smola \(2023\)Automatic chain of thought prompting in large language models\.ICLR\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p2.1)\.
- Z\. Zhang, J\. Xu, Z\. He, T\. Liang, Q\. Liu, Y\. Li, L\. Song, Z\. Liang, Z\. Zhang, R\. Wang,et al\.\(2025c\)Deeptheorem: advancing llm reasoning for theorem proving through natural language and reinforcement learning\.arXiv preprint arXiv:2505\.23754\.Cited by:[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1)\.
- A\. Zhao, Y\. Wu, Y\. Yue, T\. Wu, Q\. Xu, M\. Lin, S\. Wang, Q\. Wu, Z\. Zheng, and G\. Huang \(2025a\)Absolute zero: reinforced self\-play reasoning with zero data\.arXiv preprint arXiv:2505\.03335\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p4.1)\.
- H\. Zhao, J\. Shen, Y\. Zhang, S\. Gao, K\. Liu, T\. Ma, F\. Zheng, D\. Lin, W\. Zhang, and K\. Chen \(2025b\)Achieving olympia\-level geometry large language model agent via complexity boosting reinforcement learning\.arXiv preprint arXiv:2512\.10534\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1)\.
- H\. Zhao, Y\. Geng, S\. Tang, Y\. Lin, B\. Lyu, H\. Lin, C\. Jin, and S\. Arora \(2025c\)Ineq\-comp: benchmarking human\-intuitive compositional reasoning in automated theorem proving on inequalities\.Cited by:[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.8.1)\.
- X\. Zhao, W\. Li, and L\. Kong \(2023\)Decomposing the enigma: subgoal\-based demonstration learning for formal theorem proving\.arXiv preprint arXiv:2305\.16366\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1)\.
- X\. Zhao, L\. Zheng, H\. Bo, C\. Hu, U\. Thakker, and L\. Kong \(2024\)SubgoalXL: subgoal\-based expert learning for theorem proving\.arXiv preprint arXiv:2408\.11172\.Cited by:[§B\.3](https://arxiv.org/html/2607.07779#A2.SS3.SSS0.Px2.p1.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1)\.
- C\. Zheng, H\. Wang, E\. Xie, Z\. Liu, J\. Sun, H\. Xin, J\. Shen, Z\. Li, and Y\. Li \(2024\)Lyra: orchestrating dual correction in automated theorem proving\.Transactions on Machine Learning Research\.Cited by:[§B\.5](https://arxiv.org/html/2607.07779#A2.SS5.p4.1),[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1)\.
- K\. Zheng, J\. M\. Han, and S\. Polu \(2022\)MiniF2F: a cross\-system benchmark for formal olympiad\-level mathematics\.InInternational Conference on Learning Representations,Cited by:[§A\.1](https://arxiv.org/html/2607.07779#A1.SS1.p1.1),[§1](https://arxiv.org/html/2607.07779#S1.p3.1),[§2\.8](https://arxiv.org/html/2607.07779#S2.SS8.p3.1),[Table 3](https://arxiv.org/html/2607.07779#S2.T3.1.1.2.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1)\.
- A\. Zhou, K\. Yan, M\. Shlapentokh\-Rothman, H\. Wang, and Y\. Wang \(2024\)Language agent tree search unifies reasoning, acting, and planning in language models\.InProceedings of the 41st International Conference on Machine Learning,pp\. 62138–62160\.Cited by:[§2\.4](https://arxiv.org/html/2607.07779#S2.SS4.p3.1)\.
- Y\. Zhou, J\. Zhao, Y\. Zhang, B\. Wang, S\. Wang, L\. Chen, J\. Wang, H\. Chen, A\. Jie, X\. Zhang,et al\.\(2025\)Solving formal math problems by decomposition and iterative reflection\.arXiv preprint arXiv:2507\.15225\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p3.1),[§3\.2](https://arxiv.org/html/2607.07779#S3.SS2.p2.1),[Table 4](https://arxiv.org/html/2607.07779#S4.T4.1.1.4.1)\.
- M\. Zhu, Z\. Wang, S\. Ji, Z\. Du, J\. Ke, X\. Deng, Z\. Yin, X\. Huang, H\. Wang, and W\. Chen \(2025a\)GenesisGeo: technical report\.arXiv preprint arXiv:2509\.21896\.Cited by:[§B\.4](https://arxiv.org/html/2607.07779#A2.SS4.p2.1)\.
- T\. Zhu, J\. Clune, J\. Avigad, A\. Q\. Jiang, and S\. Welleck \(2025b\)Premise selection for a lean hammer\.arXiv preprint arXiv:2506\.07477\.Cited by:[§5\.4](https://arxiv.org/html/2607.07779#S5.SS4.p1.1)\.
- M\. Zimmer, X\. Ji, R\. Tutunov, A\. Bordg, J\. Wang, and H\. B\. Ammar \(2025\)Bourbaki: self\-generated and goal\-conditioned mdps for theorem proving\.arXiv preprint arXiv:2507\.02726\.Cited by:[§3\.1\.2](https://arxiv.org/html/2607.07779#S3.SS1.SSS2.p2.1)\.

## Appendix Overview

This appendix provides supplementary material that complements the main paper:

- [A](https://arxiv.org/html/2607.07779#A1)Extended Benchmark and Evaluation Analysis— Datasets, evaluation metrics, and ITP comparison
- [B](https://arxiv.org/html/2607.07779#A2)Extended Taxonomy of Recent Methods— Detailed method categorization and technical comparisons
- [C](https://arxiv.org/html/2607.07779#A3)Case Studies and Failure Analysis— Autoformalization examples and failure mode taxonomy

## Appendix AExtended Benchmark and Evaluation Analysis

This section provides detailed analysis of the benchmarks, datasets, and evaluation methodologies referenced in the main paper, examining their design philosophies, technical metrics, and the landscape of interactive theorem provers\.

### A\.1Benchmark Design Philosophies and Characteristics

The miniF2F benchmark\[Zhenget al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib9)\]has emerged as the de facto standard for evaluating neural theorem provers, and understanding its design philosophy illuminates both its strengths and limitations\. Created by OpenAI researchers, miniF2F comprises 488 problems \(split equally between validation and test sets\) drawn from high school mathematics competitions including the AMC, AIME, and IMO\. A distinctive feature is its cross\-lingual nature: each problem is formalized in Lean, Isabelle, and Metamath, enabling direct comparison across proof assistants\. This design choice reflects an aspiration toward language\-agnostic theorem proving capabilities\. However, the relatively small size and focus on competition mathematics limits its ability to assess progress toward research\-level proving\. Recent critical analysis\[Ospanovet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib34)\]has revealed that over half of the problems contain discrepancies between their natural language statements and formal specifications, a sobering finding that suggests benchmark scores may not accurately reflect true autoformalization and proving capabilities\.

PutnamBench\[Tsoukalaset al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib74)\]addresses the difficulty ceiling limitation by targeting the William Lowell Putnam Mathematical Competition, the premier undergraduate mathematics competition in North America\. Its 690 problems present significantly harder challenges than miniF2F, requiring deeper mathematical maturity, longer chains of reasoning, and often creative insights that go beyond standard techniques\. The benchmark spans Lean, Isabelle, and Coq, again enabling cross\-system comparison\. PutnamBench represents an important step toward research\-level evaluation, though competition mathematics still differs fundamentally from open\-ended research problems in that solutions are known to exist and problems are designed to be solvable within time constraints\.

Several recent benchmarks have attempted to push further toward research\-level evaluation\. FrontierMath\[Glazeret al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib198)\]explicitly targets problems at the frontier of mathematical research, though its closed nature limits community evaluation and reproducibility\. The Formal Conjectures repository\[Deepmind,[2026](https://arxiv.org/html/2607.07779#bib.bib7)\]from DeepMind provides an ongoing collection of formalized research problems, creating a living benchmark that evolves with the field\. FATE\[Jianget al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib28)\]targets graduate\-level algebra drawn from the Stacks Project, representing mathematics significantly beyond competition level\. These benchmarks collectively push the evaluation frontier closer to genuine research mathematics, though substantial gaps remain\.

### A\.2Dataset Quality and Fidelity Considerations

Our survey of the literature identifies several quality challenges that must be addressed as benchmarks mature\. The most fundamental is statement fidelity, the alignment between informal mathematical intent and formal specification: small choices about quantifier scope, implicit assumptions, type encodings, or library definitions can substantially alter a statement’s meaning, making it stronger, weaker, or different from what was intended, a pervasive issue illustrated by the miniF2F analysis\. Library dependence further threatens benchmark longevity, since formalizations are tied to evolving libraries such as mathlib, where refactoring, renaming, and definitional changes can require substantial maintenance or even change mathematical content, as seen in the Lean 3 to Lean 4 and mathlib to mathlib4 transitions\. Finally, difficulty calibration complicates interpretation, as human\-assigned difficulty often misaligns with computational difficulty for neural provers: problems deemed hard may reduce to pattern matching, while ostensibly simple ones may require novel insights, motivating evaluation protocols that emphasize capability profiles over single aggregate scores\.

### A\.3Evaluation Metrics

This subsection provides precise definitions of evaluation metrics used throughout the neural theorem proving literature, enabling accurate interpretation and comparison of reported results\.

Measuring success in these tasks requires metrics that capture logical correctness rather than mere textual similarity\. For autoformalization, standard n\-gram metrics like BLEU\[Papineniet al\.,[2002](https://arxiv.org/html/2607.07779#bib.bib31)\]are often misleading due to the syntactic flexibility of formal languages; while type\-checking offers a minimum bar for validity, the gold standard remainsSemantic EquivalenceMoore and Shah \[[2025](https://arxiv.org/html/2607.07779#bib.bib33)\], which formally verifies that the generated statement logically implies the reference\. In the domain of proof generation,Pass@kis the dominant metric, capturing both the precision of a model \(at lowkk\) and its exploration potential \(at highkk\)\. Furthermore, resource metrics such as proof length and search efficiency \(e\.g\., nodes expanded\) are becoming increasingly critical to distinguish practical, efficient solvers from those that rely on prohibitive computational resources\.

##### Pass@k for Proof Generation\.

The Pass@k metric measures the probability that at least one ofkkproof attempts succeeds\. For a problem where the model has per\-attempt success probabilitypp, the expected Pass@k is1−\(1−p\)k1\-\(1\-p\)^\{k\}\. In practice, we estimate Pass@k fromnntotal samples withccsuccesses using the unbiased estimator:

Pass@​k^=1−\(n−ck\)\(nk\)\\widehat\{\\text\{Pass@\}k\}=1\-\\frac\{\\binom\{n\-c\}\{k\}\}\{\\binom\{n\}\{k\}\}\(1\)This accounts for sampling without replacement\. Whenn≫kn\\gg k, this simplifies to1−\(1−c/n\)k1\-\(1\-c/n\)^\{k\}\. Pass@1 indicates single\-attempt reliability \(greedy decoding\), while Pass@64 or Pass@100 reveals ceiling performance with extensive search\. The gap between Pass@1 and high\-kkvalues indicates how much the model benefits from exploration, a large gap suggests correct proofs exist in the model’s distribution but are not reliably sampled\.

##### Semantic Equivalence for Autoformalization\.

Evaluating autoformalization requires determining whether generated statementGGcaptures the same content as referenceRR\. Surface metrics like BLEU poorly capture semantic correctness since syntactically different statements may be logically equivalent\. The gold standard is semantic equivalence, verified by proving both implications:

G⇔Riff\(G⟹R\)∧\(R⟹G\)G\\Leftrightarrow R\\quad\\text\{iff\}\\quad\(G\\implies R\)\\land\(R\\implies G\)\(2\)This correctly handles valid alternative formalizations\. However, semantic equivalence checking is computationally expensive and may fail for equivalent statements using incompatible library abstractions\.

##### Efficiency Metrics\.

Beyond success rates, practical systems require efficiency analysis: proof attempts per success \(tactics tried before finding a proof\), search nodes expanded \(for tree search\), wall\-clock time \(including ITP overhead\), and token consumption \(LLM inference cost\)\. These metrics distinguish systems that find proofs through exhaustive exploration from those that navigate efficiently to solutions\.

## Appendix BExtended Taxonomy of Recent Methods

This section supplements the taxonomy presented in the main paper \(Section[3](https://arxiv.org/html/2607.07779#S3)\) with additional technical details, method comparisons, and discussion of emerging hybrid approaches\.

### B\.1Training Paradigms: A Technical Comparison

Neural theorem provers employ diverse training strategies, each with distinct characteristics that impact performance, sample efficiency, and generalization\. We provide detailed comparisons below\.

##### Supervised Fine\-Tuning \(SFT\)\.

SFT adapts pretrained LLMs to theorem proving via behavioral cloning on human\-written proof traces\. Given a dataset of\(st,at\)\(s\_\{t\},a\_\{t\}\)pairs, wherests\_\{t\}is the proof state andata\_\{t\}is the expert tactic, the model minimizes:

ℒSFT=−𝔼\(s,a\)∼𝒟​\[log⁡πθ​\(a∣s\)\]\\mathcal\{L\}\_\{\\text\{SFT\}\}=\-\\mathbb\{E\}\_\{\(s,a\)\\sim\\mathcal\{D\}\}\\left\[\\log\\pi\_\{\\theta\}\(a\\mid s\)\\right\]\(3\)SFT provides stable training and leverages decades of formalized mathematics without RL’s hyperparameter sensitivity\. However, as imitation learning, it cannot discover strategies absent from training data\. Systems like PALM\[Luet al\.,[2024d](https://arxiv.org/html/2607.07779#bib.bib35)\], InternLM\-StepProver\[Wuet al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib69)\], and Goedel\-Prover\[Linet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib64)\]demonstrate that careful data curation, emphasizing quality over quantity, can substantially improve SFT performance\.

##### Expert Iteration\.

Expert iteration alternates between proof search and policy improvement, bootstrapping beyond the initial training distribution\. Each round: \(1\) uses the current policy with search \(sampling, beam, or tree\) to attempt theorems; \(2\) retains only verified proof traces; \(3\) fine\-tunes the policy on successful proofs\. Formally, roundiiproduces policyπi\\pi\_\{i\}from data𝒟i=𝒟i−1∪Search​\(πi−1\)\\mathcal\{D\}\_\{i\}=\\mathcal\{D\}\_\{i\-1\}\\cup\\text\{Search\}\(\\pi\_\{i\-1\}\)\. The DeepSeek\-Prover series\[Xinet al\.,[2024a](https://arxiv.org/html/2607.07779#bib.bib60),[b](https://arxiv.org/html/2607.07779#bib.bib61); Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]exemplifies this approach, progressively improving through multiple iterations\. AlphaProof\[DeepMind,[2024](https://arxiv.org/html/2607.07779#bib.bib82)\]scales expert iteration with massive compute, while open systems like SEED\-Prover\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\]and Leanabell\-Prover\[Zhanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib65)\]demonstrate accessibility of this paradigm\.

##### Policy Gradient Methods\.

Direct RL optimization using policy gradients enables learning from sparse theorem\-level rewards\. While PPO\[Schulmanet al\.,[2017](https://arxiv.org/html/2607.07779#bib.bib80)\]remains popular due to its stability, recent work has introduced more efficient alternatives\. Group Relative Policy Optimization \(GRPO\)\[DeepSeek\-AI,[2025](https://arxiv.org/html/2607.07779#bib.bib84)\]eliminates the critic network by using group\-relative advantages:

𝒥GRPO​\(θ\)=𝔼q,\{oi\}i=1G∼πθold​\[1G​∑i=1Gmin⁡\(ri​\(θ\)​A^i,clip​\(ri​\(θ\),1−ϵ,1\+ϵ\)​A^i\)\]−β​DKL​\(πθ∥πref\)\\mathcal\{J\}\_\{\\text\{GRPO\}\}\(\\theta\)=\\mathbb\{E\}\_\{q,\\\{o\_\{i\}\\\}\_\{i=1\}^\{G\}\\sim\\pi\_\{\\theta\_\{\\text\{old\}\}\}\}\\left\[\\frac\{1\}\{G\}\\sum\_\{i=1\}^\{G\}\\min\\left\(r\_\{i\}\(\\theta\)\\hat\{A\}\_\{i\},\\text\{clip\}\(r\_\{i\}\(\\theta\),1\{\-\}\\epsilon,1\{\+\}\\epsilon\)\\hat\{A\}\_\{i\}\\right\)\\right\]\-\\beta D\_\{\\text\{KL\}\}\(\\pi\_\{\\theta\}\\\|\\pi\_\{\\text\{ref\}\}\)\(4\)whereri​\(θ\)=πθ​\(oi\|q\)/πθold​\(oi\|q\)r\_\{i\}\(\\theta\)=\\pi\_\{\\theta\}\(o\_\{i\}\|q\)/\\pi\_\{\\theta\_\{\\text\{old\}\}\}\(o\_\{i\}\|q\)is the importance ratio, and the group\-relative advantage is computed asA^i=\(Ri−mean​\(\{Rj\}\)\)/std​\(\{Rj\}\)\\hat\{A\}\_\{i\}=\(R\_\{i\}\-\\text\{mean\}\(\\\{R\_\{j\}\\\}\)\)/\\text\{std\}\(\\\{R\_\{j\}\\\}\), normalizing rewards within a batch ofGGsampled outputs\. This formulation avoids training a separate value function while providing stable policy updates\. Kimina\-Prover\[Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68)\]combines GRPO with large reasoning model architectures for improved exploration in formal theorem proving\.

### B\.2Search Algorithms: Detailed Analysis

Search strategy critically determines whether neural provers succeed, controlling exploration of the proof state space\.

##### Best\-First Search\.

Best\-first search maintains a priority queue of proof states, expanding the most promising state according to a learned value functionVθ​\(s\)V\_\{\\theta\}\(s\)or policy confidence\. BFS\-Prover\[Xinet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib63)\]refines this with carefully engineered heuristics\. The simplicity of best\-first search makes it efficient for problems where the value function accurately predicts proof feasibility, but it can struggle when good proofs require initially unpromising steps\.

##### Monte Carlo Tree Search \(MCTS\)\.

MCTS frames proof search as sequential decision\-making, balancing exploration and exploitation through the UCB formula:

UCB​\(s,a\)=Q​\(s,a\)\+c⋅πθ​\(a\|s\)⋅∑bN​\(s,b\)1\+N​\(s,a\)\\text\{UCB\}\(s,a\)=Q\(s,a\)\+c\\cdot\\pi\_\{\\theta\}\(a\|s\)\\cdot\\frac\{\\sqrt\{\\sum\_\{b\}N\(s,b\)\}\}\{1\+N\(s,a\)\}\(5\)whereQ​\(s,a\)Q\(s,a\)is the estimated value,πθ​\(a\|s\)\\pi\_\{\\theta\}\(a\|s\)is the policy prior, andN​\(s,a\)N\(s,a\)is the visit count\. HyperTree\[Lampleet al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib59)\]pioneered MCTS for theorem proving, demonstrating scalability to deep proof trees\. DeepSeek\-Prover\-V1\.5\[Xinet al\.,[2024b](https://arxiv.org/html/2607.07779#bib.bib61)\]uses MCTS not just for inference but as a data generation mechanism, aligning LLMs with verification feedback\.

##### Hybrid Neuro\-Symbolic Search\.

Thor\[Jianget al\.,[2022](https://arxiv.org/html/2607.07779#bib.bib94)\]integrates neural tactic prediction with Sledgehammer’s ATP backend, using the LLM to select promising lemmas and the symbolic prover to discharge goals\. This division of labor, neural creativity for strategic choices, symbolic reliability for routine steps—exemplifies the hybrid paradigm increasingly adopted by state\-of\-the\-art systems\.

### B\.3Agentic and Hierarchical Approaches

Recent work increasingly treats theorem proving as an agent task requiring planning, tool use, and strategic reasoning\.

##### Tool\-Augmented Proving\.

Agentic provers leverage external tools beyond the ITP itself\. SEED\-Prover 1\.5\[Chenet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib170)\]integrates formal library retrieval with Python execution for computational verification\. LTRAG\[Huet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib24)\]and LemmaHead\[Yanget al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib19)\]use retrieval\-augmented generation to ground proof attempts in relevant library content, reducing hallucination of non\-existent lemmas\.

##### Hierarchical Decomposition\.

The Draft\-Sketch\-Prove paradigm\[Jianget al\.,[2023b](https://arxiv.org/html/2607.07779#bib.bib15); Caoet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib101)\]structures proof generation as: \(1\) draft an informal proof sketch; \(2\) translate to formal intermediate structure; \(3\) fill in tactic\-level details\. This mirrors human mathematical practice, where high\-level strategy precedes low\-level formalization\. SubgoalXL\[Zhaoet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib72)\]trains models explicitly on subgoal generation, while DeepSeek\-Prover\-V2\[Renet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib62)\]uses RL to learn productive decomposition strategies\.

##### Multi\-Agent Collaboration\.

MASA\[Zhanget al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib23)\]deploys specialized agents for distinct subtasks: parsing informal statements, searching libraries, generating formalizations, and verifying correctness\. This specialization enables each agent to develop expertise in its domain while collaborative protocols coordinate the overall proving process\.

### B\.4Geometry\-Specific Methods

Geometric theorem proving employs specialized representations and algorithms distinct from general\-purpose approaches\. Existing approaches to automated geometric theorem proving, exemplified by AlphaGeometry\[Trinhet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib85)\], favor geometry\-specific languages over general\-purpose proof assistants such as Lean\[de Moura and Ullrich,[2021](https://arxiv.org/html/2607.07779#bib.bib52)\], as these tools better capture geometric primitives and constructions, support efficient search, and naturally fall into algebraic and synthetic paradigms\. In algebraic methods, a geometry problem is formulated as a system of polynomial equations and solved via Wu’s method\[Wu,[2008](https://arxiv.org/html/2607.07779#bib.bib159); Chou,[1988](https://arxiv.org/html/2607.07779#bib.bib187)\]or Gröbner basis techniques\[Lazard,[1983](https://arxiv.org/html/2607.07779#bib.bib188)\]\. For synthetic methods,Chouet al\.\[[1993](https://arxiv.org/html/2607.07779#bib.bib36)\]used the area method to generate human\-readable proofs for more than 400 problems, whileChouet al\.\[[2000](https://arxiv.org/html/2607.07779#bib.bib37)\]developed a deductive database \(DD\) built upon a collection of geometric inference rules\.

Building on synthetic methods, AlphaGeometry\[Trinhet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib85)\]improves theDD method with an additional algebraic engine\(DDAR\) and employs a neural network to add extra auxiliary points for geometry problems, solving 25 problems on the IMO\-30 benchmark\. When combined with Wu’s method\[Sinhaet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib189)\], which independently solves 15 of the 30 problems on IMO\-30, AlphaGeometry can solve 27/30 problems\. Further advances include TongGeometry\[Zhanget al\.,[2026](https://arxiv.org/html/2607.07779#bib.bib44)\], which enhances AlphaGeometry’s DD with a tree\-search\-based framework, as well as AlphaGeometry2\[Chervonyiet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib86)\]and Seed\-Geometry\[Chenet al\.,[2025c](https://arxiv.org/html/2607.07779#bib.bib102)\], which advance the system through enhancements to the geometric language, improved DDAR efficiency, and ensemble LLM guidance\. More recently, GenesisGeo\[Zhuet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib191)\]introduces an optimized DDARN engine with efficient neuro\-symbolic reasoning, while HAGeo\[Duanet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib186)\]proposes a CPU\-only DDAR system with efficient auxiliary constructions that achieve IMO gold\-medal performance\. InternGeometry\[Zhaoet al\.,[2025b](https://arxiv.org/html/2607.07779#bib.bib193)\]proposes training LLMs with RL for auxiliary construction and geometric deduction, and using the trained models within an agent\-based workflow\.

##### Algebraic Methods\.

Wu’s method\[Wu,[2008](https://arxiv.org/html/2607.07779#bib.bib159)\]and Gröbner basis techniques\[Lazard,[1983](https://arxiv.org/html/2607.07779#bib.bib188)\]formulate geometry problems as polynomial systems\. These methods are complete for the algebraic fragment of geometry but produce proofs that are often non\-human\-readable\.

##### Synthetic Methods\.

The deductive database \(DD\) approach\[Chouet al\.,[2000](https://arxiv.org/html/2607.07779#bib.bib37)\]applies geometric inference rules to derive new facts from known ones\. AlphaGeometry\[Trinhet al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib85)\]augments DD with neural auxiliary point construction, solving 25/30 IMO geometry problems\. AlphaGeometry2\[Chervonyiet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib86)\]and HAGeo\[Duanet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib186)\]further improve through enhanced geometric languages and more efficient deduction engines, with HAGeo achieving gold\-medal performance on IMO geometry\.

### B\.5Emerging Directions

Several trends point toward future developments:

Large Formal Reasoning Models\.Kimina\-Prover\[Wanget al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib68)\]and similar systems combine the extended reasoning capabilities of LRMs \(like DeepSeek\-R1\) with formal verification, generating lengthy “thinking” chains before committing to formal tactics\.

Lifelong Learning\.LeanAgent\[Kumarappanet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib90)\]maintains and updates strategies across proof attempts, accumulating reusable knowledge that biases future searches toward successful patterns\.

Self\-Correction\.HybridProver\[Huet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib25)\], ReForm\[Chenet al\.,[2025a](https://arxiv.org/html/2607.07779#bib.bib26)\], and Lyra\[Zhenget al\.,[2024](https://arxiv.org/html/2607.07779#bib.bib73)\]implement iterative refinement loops where models diagnose and fix their own proof errors, moving toward more robust proving through self\-improvement\.

## Appendix CCase Studies and Failure Analysis

This section provides concrete examples illustrating the semantic gap between informal and formal mathematics, followed by a taxonomy of common failure modes in neural theorem proving\. Together, these case studies ground the abstract challenges discussed in the main paper\.

### C\.1Autoformalization Case Studies

#### C\.1\.1Example 1: Implicit Quantification and Domain Constraint

Consider the familiar theorem from real analysis: “Every continuous function on a closed interval attains its maximum\.” This statement appears unambiguous to any mathematician, yet formalizing it requires making numerous implicit assumptions explicit\.

A valid Lean 4 formalization might read:

theoremcontinuous\_attains\_max

\{f:ℝ\\mathbb\{R\}→\\toℝ\\mathbb\{R\}\}\{ab:ℝ\\mathbb\{R\}\}\(hab:a≤\\leqb\)

\(hf:ContinuousOnf\(Set\.Iccab\)\):

∃\\existsx∈\\inSet\.Iccab,∀\\forally∈\\inSet\.Iccab,

fy≤\\leqfx:=by

exactIsCompact\.exists\_isMaxOn

isCompact\_Icc<a,left\_mem\_Icc\.mprhab\>hf

This formalization reveals several implicit elements in the informal statement\. First, the requirement thata≤ba\\leq bis unstated but necessary—an “interval”\[b,a\]\[b,a\]withb\>ab\>awould be empty, making the theorem vacuously true but mathematically uninteresting\. Second, the domain is implicitlyℝ\\mathbb\{R\}; the theorem generalizes to other contexts but requires different formulations\. Third, “continuous” must be interpreted asContinuousOnrather than global continuity, since the function need only be continuous on the interval\. Fourth, the interval\[a,b\]\[a,b\]maps to the mathlib typeSet\.Icc a b, one of several possible interval representations\. Finally, the proof invokes compactness of closed bounded intervals \(isCompact\_Icc\), a fact the informal statement implicitly relies upon but does not mention\.

An autoformalization system must make all these choices correctly, and different choices can yield statements that are strictly stronger, strictly weaker, or simply different from the intended claim\.

#### C\.1\.2Example 2: Notation Ambiguity and Indexing Conventions

The Basel problem provides a classic example of notation\-induced ambiguity: “∑n=1∞1n2=π26\\sum\_\{n=1\}^\{\\infty\}\\frac\{1\}\{n^\{2\}\}=\\frac\{\\pi^\{2\}\}\{6\}”

In Lean 4, this might be formalized as:

theorembasel\_problem:

∑\\sum’n:ℕ\\mathbb\{N\},\(1:ℝ\\mathbb\{R\}\)/\(n\+1\)^2=π\\pi^2/6:=by

exactReal\.tsum\_inv\_nat\_sq

Several non\-obvious choices appear in this formalization\. The informal indexing starts atn=1n=1, but Lean’s natural numbers begin at 0, necessitating the shift to\(n\+1\)\(n\+1\)in the formal version\. The informal summation symbol∑\\sumbecomestsum\(topological sum\), the appropriate notion for infinite series in mathlib’s analysis library\. The type annotation1∈ℝ1\\in\\mathbb\{R\}is essential to ensure real\-valued computation; without it, Lean might interpret the division in the natural numbers, yielding incorrect results\. These details, invisible in informal mathematics, must be precisely specified for formal verification\.

#### C\.1\.3Example 3: The Specification Fidelity Problem

The main paper mentions Aristotle\[Achimet al\.,[2025](https://arxiv.org/html/2607.07779#bib.bib199)\]as an example of the specification gap problem\. This case merits detailed examination because it illustrates how formal verification can provide false confidence when the verified statement does not match the intended mathematical claim\.

In late 2025, Aristotle reportedly produced a machine\-verified proof for a problem from the Erdős problem database\. Initial announcements suggested a significant breakthrough—an AI system had resolved a long\-standing open problem\. However, closer examination revealed a critical issue: the formalized statement omitted key constraints present in the original conjecture\. The verified claim was a weaker, related statement that does not resolve the original problem\.

This case illustrates several important lessons for the field\. First, formal verification confirms logical consistency but cannot assess semantic fidelity to informal intent\. The proof was completely valid for the statement actually formalized; the error lay in the formalization itself, not the proving process\. Second, when AI systems claim to solve open problems, independent verification of statement fidelity becomes essential\. The workflow should include explicit confirmation that the formal statement matches the problem’s mathematical content, ideally by domain experts familiar with the original conjecture\. Third, this failure mode will become increasingly common as systems tackle more ambitious problems where ground truth is unavailable\. For competition problems, reference formalizations exist to compare against; for open problems, no such safety net exists, placing greater responsibility on the formalization step\.

The broader implication is that research\-level formal mathematics requires not just powerful provers but also robust autoformalization with human\-in\-the\-loop verification for high\-stakes claims\. Machine verification of an incorrect specification provides false confidence that may be worse than no verification at all\.

#### C\.1\.4Example 4: Library Definition Choices

Consider formalizing “the limit off​\(x\)f\(x\)asxxapproachesaaequalsLL\.” Even this basic calculus concept admits multiple formalizations depending on library choices:

\-\-UsingFilter\.Tendsto

example:Filter\.Tendstof\(nhdsa\)\(nhdsL\):=\.\.\.

\-\-UsingMetric\.tendsto\_atTopforsequences

example:Metric\.TendstofFilter\.atTop\(nhdsL\):=\.\.\.

\-\-Explicitepsilon\-delta

example:∀\\forallε\\varepsilon\>0,∃\\existsδ\\delta\>0,∀\\forallx,\|x\-a\|<δ\\delta→\\to

\|fx\-L\|<ε\\varepsilon:=\.\.\.

These formalizations are mathematically equivalent but use different library abstractions\. An autoformalization system must choose the representation that best matches both the informal intent and the available proof strategies\. Using the “wrong” equivalent formulation may make subsequent proving dramatically harder if relevant lemmas are stated in terms of a different representation\.

### C\.2Failure Mode Taxonomy

![Refer to caption](https://arxiv.org/html/2607.07779v1/x9.png)Figure 10:Common failure cases in LLM\-driven formal mathematics\.Illustrative examples of how errors introduced during translation and proof construction \(e\.g\., missing implicit constraints, ambiguous notation/indexing, specification drift, or mismatched library choices\) propagate into different downstream failure types \(syntactic, semantic, search, and strategic\) across autoformalization, prover search, and the Lean environment\.Understanding how neural theorem provers fail guides improvement efforts\. We categorize common failure modes:

Syntactic Failuresoccur when generated tactics are ill\-formed: type errors \(applying lemmas to incorrectly\-typed terms\), name resolution failures \(referencing non\-existent library content\), or malformed syntax\. These are caught immediately by the ITP but waste search budget\.*Case 1 \(Implicit Quantification and Domain Constraints\)*exemplifies this failure mode: informal mathematics often omits domain assumptions \(e\.g\., implicitly assumingn\>0n\>0before division\), but Lean requires such constraints to be made explicit\. When these assumptions are missing, the proof fails syntactically despite the underlying mathematical idea being correct, wasting search budget on trivial well\-formedness issues\.

Semantic Failuresinvolve syntactically valid but unproductive tactics: invalid applications \(correct lemma, wrong arguments\), circular reasoning \(returning to previous states\), or goal drift \(transforming goals into harder equivalent forms\)\. These are harder to detect and may consume substantial search effort\.*Case 2 \(Notation Ambiguity and Indexing Conventions\)*highlights this issue: informal summation notation often hides indexing conventions, and small mismatches \(e\.g\., summing over\{0,…,n−1\}\\\{0,\\dots,n\-1\\\}versus\{0,…,n\}\\\{0,\\dots,n\\\}\) lead to well\-typed but incorrect formal goals\.*Case 3 \(Specification Infidelity\)*represents a more severe semantic failure, where missing or weakened hypotheses cause the formalized statement to diverge from the intended theorem\. In such cases, Lean may successfully verify a proof that exploits degenerate cases \(e\.g\.,n=0n=0\), yielding a formally correct proof of the wrong statement\.

Strategic Failuresreflect wrong high\-level choices: attempting direct proof when induction is required, missing necessary case splits, or failing to recognize applicable library lemmas\. These often require abandoning partial proofs entirely\.*Case 4 \(Library Definition Choices\)*illustrates this failure mode: formal libraries often provide multiple non\-interchangeable definitions for similar concepts \(e\.g\.,Nat\.PrimeversusPrime\), and selecting the wrong abstraction can introduce coercions, incompatibilities, or dead ends that require abandoning partial proofs and replanning at a global level\.

Search Failuresoccur even when correct proofs exist within capability: timeouts \(budget exhausted\), diversity collapse \(sampling produces redundant tactics\), or local minima \(committing to suboptimal paths\)\. These motivate better search algorithms and value estimation\.

Understanding these failure categories helps practitioners diagnose system limitations and researchers prioritize improvements\. Syntactic failures suggest training data or architecture issues; strategic failures indicate deficits in high\-level planning; search failures call for better exploration algorithms\.

##### Competition\-level and Research\-level Formal Representation Gap\.

We illustrate the representational gap between competition\-level and research\-level mathematical problems in formal and informal settings\.

- •Competition\-level problem Informal \(natural language\): > IMO 2025 Problem 1\.A line in the plane is called*sunny*if it is not parallel to any of thexx\-axis, theyy\-axis, and the linex\+y=0x\+y=0\. Letn≥3n\\geq 3be a given integer\. Determine all nonnegative integerskksuch that there existnndistinct lines in the plane satisfying: - –for all positive integersa,ba,bwitha\+b≤n\+1a\+b\\leq n\+1, the point\(a,b\)\(a,b\)lies on at least one of the lines; and - –exactlykkof thennlines are sunny\. Formal \(Lean4 excerpt\): importMathlib namespaceImo2025P1 openscopedAffineFinset openModule defxAxis:AffineSubspaceℝ\\mathbb\{R\}\(EuclideanSpaceℝ\\mathbb\{R\}\(Fin2\)\)where carrier:=\{p\|p1=0\} smul\_vsub\_vadd\_memcp1p2p3hp1hp2hp3:=bysimp\_all defyAxis:AffineSubspaceℝ\\mathbb\{R\}\(EuclideanSpaceℝ\\mathbb\{R\}\(Fin2\)\)where carrier:=\{p\|p0=0\} smul\_vsub\_vadd\_memcp1p2p3hp1hp2hp3:=bysimp\_all deflinexy0:AffineSubspaceℝ\\mathbb\{R\}\(EuclideanSpaceℝ\\mathbb\{R\}\(Fin2\)\)where carrier:=\{p\|p0\+p1=0\} smul\_vsub\_vadd\_memcp1p2p3hp1hp2hp3:=by simponly\[Fin\.isValue,vsub\_eq\_sub,vadd\_eq\_add,Set\.mem\_setOf\_eq,PiLp\.add\_apply, PiLp\.smul\_apply,PiLp\.sub\_apply,smul\_eq\_mul\] sufficesc\*\(p10\+p11\-\(p20\+p21\)\)\+\(p30\+p31\)=0by rw\[←\\leftarrowthis\] ring simp\_all defSunny\(s:AffineSubspaceℝ\\mathbb\{R\}\(EuclideanSpaceℝ\\mathbb\{R\}\(Fin2\)\)\):Prop:= ¬\\negs∥\\parallelxAxis∧\\land¬\\negs∥\\parallelyAxis∧\\land¬\\negs∥\\parallellinexy0 noncomputabledefsunnyPred:DecidablePredSunny:=Classical\.decPred\_ /\-determine\-/abbrevanswer:Set\.Ici3→\\toSetℕ\\mathbb\{N\}:=sorry theoremimo2025\_p1\(n:Set\.Ici3\): \{k\|∃\\existslines:Finset\(AffineSubspaceℝ\\mathbb\{R\}\(EuclideanSpaceℝ\\mathbb\{R\}\(Fin2\)\)\), have:=sunnyPred; \#lines=n∧\\land\(∀\\foralll∈\\inlines,finrankℝ\\mathbb\{R\}l\.direction=1\)∧\\land \(∀\\forallab:ℕ\\mathbb\{N\},0<a→\\to0<b→\\toa\+b≤\\leq\(n:ℕ\\mathbb\{N\}\)\+1→\\to∃\\existsl∈\\inlines,\!2\[\(a:ℝ\\mathbb\{R\}\),b\]∈\\inl\)∧\\land \#\{l∈\\inlines\|Sunnyl\}=k\}=answern:=sorry endImo2025P1
- •Research\-level problem Informal \(natural language\): > Erdős Problem 12 LetAAbe an infinite set such that there are no distincta,b,c∈Aa,b,c\\in Asuch thata∣\(b\+c\)a\\mid\(b\+c\)andb,c\>ab,c\>a\. Is there such anAAwith lim infN→∞\|A∩\{1,…,N\}\|N1/2\>0​?\\liminf\_\{N\\to\\infty\}\\frac\{\\lvert A\\cap\\\{1,\\ldots,N\\\}\\rvert\}\{N^\{1/2\}\}\>0\\,?Does there exist some absolute constantc\>0c\>0such that there are always infinitely manyNNwith \|A∩\{1,…,N\}\|<N1−c​?\\lvert A\\cap\\\{1,\\ldots,N\\\}\\rvert<N^\{\\,1\-c\}\\,?Is it true that ∑n∈A1n<∞​?\\sum\_\{n\\in A\}\\frac\{1\}\{n\}<\\infty\\,? Formal \(Lean4 excerpt\): importFormalConjectures\.Util\.ProblemImports openClassicalFilter namespaceErdos12 abbrevIsGood\(A:Setℕ\\mathbb\{N\}\):Prop:=A\.Infinite∧\\land ∀e\\forall^\{e\}\(a∈\\inA\)\(b∈\\inA\)\(c∈\\inA\),a∣\\midb\+c→\\toa<b→\\to a<c→\\tob=c @\[categoryundergraduate,AMS11\] theoremisGoodExample: IsGood\{p^2\|\(p:ℕ\\mathbb\{N\}\)\(\_:p≡\\equiv3\[MOD4\]\)\(\_:p\.Prime\)\}:=by sorry openErdos12 @\[categoryresearchopen,AMS11\] theoremerdos\_12\.parts\.i:answer\(sorry\)↔\\leftrightarrow∃\\exists\(A:Setℕ\\mathbb\{N\}\),IsGoodA∧\\land \(0:ℝ\\mathbb\{R\}\)<Filter\.atTop\.liminf \(funN=\>\(A\.interIcc1N\)\.ncard/\(N:ℝ\\mathbb\{R\}\)\.sqrt\):=by sorry @\[categoryresearchopen,AMS11\] theoremerdos\_12\.parts\.ii:answer\(sorry\)↔\\leftrightarrow∃\\existsc\>\(0:ℝ\\mathbb\{R\}\),∀\\forall\(A:Setℕ\\mathbb\{N\}\),IsGoodA→\\to \{N:ℕ\\mathbb\{N\}\|\(A\.interIcc1N\)\.ncard<\(N:ℝ\\mathbb\{R\}\)^\(1\-c\)\}\.Infinite:=by sorry @\[categoryresearchopen,AMS11\] theoremerdos\_12\.parts\.iii: answer\(sorry\)↔\\leftrightarrow∀\\forall\(A:Setℕ\\mathbb\{N\}\),IsGoodA→\\toSummable\(fun\(n:A\)↦\\mapsto\(1/n:ℝ\\mathbb\{R\}\)\):=by sorry @\[categoryresearchsolved,AMS11\] theoremerdos\_12\.variants\.erdos\_sarkozy\_density\_0\(A:Setℕ\\mathbb\{N\}\)\(hA:IsGoodA\):A\.HasDensity0:=by sorry @\[categoryresearchsolved,AMS11\] theoremerdos\_12\.variants\.erdos\_sarkozy\(f:ℕ\\mathbb\{N\}→\\toℕ\\mathbb\{N\}\)\(hf:atTop\.TendstofatTop\): ∃\\existsA,IsGoodA∧\\land\{N:ℕ\\mathbb\{N\}\|\(N:ℝ\\mathbb\{R\}\)/fN<\(A\.interIcc1N\)\.ncard\}\.Infinite:=by sorry @\[categoryresearchsolved,AMS11\] theoremerdos\_12\.variants\.example\(A:Setℕ\\mathbb\{N\}\) \(hA:A=\{p^2\|\(p:ℕ\\mathbb\{N\}\)\(\_:p\.Prime\)\(\_:p≡\\equiv3\[MOD4\]\)\}\): IsGoodA∧\\land0<atTop\.liminf\(fun\(N:ℕ\\mathbb\{N\}\)↦\\mapsto\(A\.interIcc1N\)\.ncard\*\(N:ℝ\\mathbb\{R\}\)\.log/\\sqrt\{\\phantom\{x\}\}N\):=by sorry @\[categoryresearchsolved,AMS11\] theoremerdos\_12\.variants\.schoen\(A:Setℕ\\mathbb\{N\}\)\(hA:IsGoodA\)\(hA’:A\.PairwiseNat\.Coprime\): \(funN↦\\mapsto\(\(A\.interIcc1N\)\.ncard:ℝ\\mathbb\{R\}\)\)=O\[atTop\]\(funN↦\\mapsto\(N:ℝ\\mathbb\{R\}\)^\(2/3:ℝ\\mathbb\{R\}\)\):=by sorry @\[categoryresearchsolved,AMS11\] theoremerdos\_12\.variants\.baier\(A:Setℕ\\mathbb\{N\}\)\(hA:IsGoodA\)\(hA’:A\.PairwiseNat\.Coprime\): \(funN↦\\mapsto\(\(A\.interIcc1N\)\.ncard:ℝ\\mathbb\{R\}\)\)=O\[atTop\]\(funN↦\\mapsto\(N:ℝ\\mathbb\{R\}\)^\(2/3:ℝ\\mathbb\{R\}\)/\(N:ℝ\\mathbb\{R\}\)\.log\):=by sorry endErdos12