Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification

Formal systems and Lean.  Formal systems provide computational models for manipulating formulas and deriving theorems based on symbolic inference rules. Examples include Peano arithmetic, higher-order logic,²⁵ and dependent type theory.² The consistency of these systems allows us to potentially ground AI reasoning within them, enabling the generation of feedback signals that are useful for training and evaluating AI models. Unlike human annotations, these signals can be fully automated, making them more cost-effective and dependable.

An important implementation of formal systems is proof assistants—software enabling humans to write formal proofs about mathematics or verified software. Common examples of proof assistants include Coq,² Isabelle,²⁵ and Lean. They have different logical foundations but similar user interfaces, so we use Lean as a representative example. Figure 2 shows how Lean is used to formalize mathematics. At its core, it is a programming language for writing not only conventional programs but also mathematical definitions, theorems, and proofs. Figure 2 (middle) shows a Lean file. After defining natural numbers (Nat) and addition (add), it states and proves the theorem add_zero (∀n ∊ ∈ N, 0+n =n). Lean can automatically check whether the proof is correct, that is, consistent with the theorem statement.

Theorem proving in Lean is an interactive process (Figure 2, left). It begins with the statement as the initial goal, and the user enters a proof step, known as a tactic. Lean executes the tactic, transforming the goal into a list of subgoals. The user then inspects the new goals and enters new tactics, repeating this process until there are no goals left. This process implicitly defines a proof tree whose nodes are goals and edges are tactics. The user plays a key role here. Though proof assistants like Lean were designed with human users in mind, in formal mathematical reasoning, the user can also be AI or humans in collaboration with AI.

Formalizing mathematics using Lean is like developing software (Figure 2, right). Files are organized into larger code units such as libraries and projects, which can be open sourced on GitHub and reused by other projects. For example, the formalization of cutting-edge research often builds upon the basic concepts formalized in mathlib,²² Lean’s general-purpose mathematical library.

AI meets formal mathematics.  Integrating AI with proof assistants like Lean offers mutual benefits. Proof assistants provide data and environments for AI to learn math, while AI can enhance their usability by automating simple proofs. Figure 3 outlines key tasks in this area. One of these tasks, mentioned earlier, is autoformalization, which translates informal mathematics from textbooks or papers into formal theorems and proofs. A common approach uses LLMs to learn from a handful of expert-constructed informal-formal pairs as demonstrations.³⁶ Another task is theorem proving, where AI generates formal proofs given theorem statements. Since the task requires complex reasoning and allows rigorous evaluation in Lean, it has become increasingly popular as a testbed for LLMs.^32,38

While formal reasoning offers clear benefits, it need not replace informal reasoning; rather, the two can complement each other to support complex, rigorous reasoning in a wide range of domains. For example, combining autoformalization with theorem proving can be useful for solving problems formulated in natural language.⁴⁰ We refer to the combination of formal and informal reasoning as verified reasoning in natural language.

Moreover, formal mathematics can be applied to the verification of software and hardware systems.¹⁴ Here, one specifies the correctness/security requirements as formal statements and uses theorem proving to establish that the system satisfies its requirements. AI-driven autoformalization and theorem proving can potentially facilitate this process, significantly reducing its costs. The integration of AI and verification has been explored in the formal methods community; for example, Seshia²⁸ proposed SID (structure, induction, and deduction), a framework that combines inductive and deductive reasoning. While this paper focuses primarily on these two modes of reasoning, other forms—such as counterfactual and analogical reasoning¹⁶—have also been studied in the context of mathematics and verification.

Data.  The simultaneous scaling of compute and training data has been the main driver of LLMs’ performance in various tasks. However, scaling the training data in formal mathematics is hampered by the scarcity of human-created formal proofs. The Proof Pile dataset,¹ which aggregated proofs from six different formal languages, collected only 500MB of formal proofs—orders of magnitude smaller than its informal counterparts. The issue is more pronounced in research mathematics, where even informal data is limited.

Researchers are exploring different strategies to overcome data scarcity. The first is autoformalization. We have a substantial amount of informal math data. Since formal proofs can be verified easily, if a system successfully formalizes even a small subset of the informal math data, it can iteratively self-improve by learning from the additional formal data it has created, potentially covering an increasingly larger set with each iteration. Another approach is synthetic data generation. For example, AlphaGeometry’s training data consisted solely of synthetic geometry problems and solutions.³³ Mathematical axioms entail all provable facts, in principle containing infinite data. By generating synthetic data, AI can potentially explore and learn from the vast space of possible mathematics, at a scale that can drastically surpass the pace of human-created training data. If the method can be generalized, it would help in completely new mathematical domains, where even informal data might be scarce.

Autoformalization and synthetic data were combined in AlphaProof,⁹ which autoformalized one million informal math competition problems into 100 million formal theorems, whose proofs were synthetically generated using expert iteration. It remains an open question to generalize this approach beyond domains in which a large number of human-written problems are available, for example, research mathematics. Those domains will likely require conjecturing new unseen statements.²⁶

Another promising strategy is knowledge transfer from different modalities. Specifically, code is closely related to mathematics, as both require symbolic reasoning. This similarity has been exploited to improve AI’s general mathematical capabilities, though it is still an open question how to leverage data-rich programming languages such as Python to enhance reasoning in formal mathematical languages.

Autoformalization at sceal.  Since any given theorem can be formalized in multiple equivalent ways, a major bottleneck in autoformalization is evaluating whether the autoformalized statement is logically equivalent to the ground truth. Proxy metrics such as BLEU do not correlate well with human judgment,²³ but relying on humans is not scalable. Possible ideas for better automated metrics include checking logical equivalence via automated provers.^18,23

Autoformalization extends beyond mere translation; formalizing certain problems—such as the combinatorics problem (P5) at IMO 2024^d—may necessitate complex reasoning, retrieving relevant definitions, or even formulating new ones. For such problems, it is natural to break down the reasoning process into smaller steps, for example, retrieving definitions before formalizing the statement or generating high-level sketches before formalizing the proof. We anticipate benefits from smaller steps and process supervision^19,21 and call for autoformalization to be more interactive.

Proof search and test-time compute.  Search is fundamental in many reasoning systems. Neural theorem provers often combine tactic generation with proof search. Their search strategy ranges from independent sampling of multiple candidates to sophisticated algorithms like Monte Carlo Tree Search.¹⁵ Scaling search to exploit vast test-time compute has emerged as a promising approach for both formal and informal reasoning.

Many myths and trade-offs surrounding proof search remain unexplored. Is proof search indispensable, given that generating complete proofs can achieve lower latency?⁷ For a fixed compute budget, should we use smaller models with more search steps or larger models with fewer steps?³ How do different search algorithms compare? To answer these questions and guide the development of future provers, we need a systematic evaluation of existing methods, currently lacking due to the inherent challenge in fairly evaluating theorem proving in a unified way. It is unclear how to compare provers targeting different proof assistants. Even within the same proof assistant, a prover’s performance is multifaceted and depends on resource constraints (e.g., hardware and time limits), making it difficult to consolidate performance into a single metric. A comprehensive evaluation that addresses these complexities would be immensely valuable. Despite these challenges, researchers are exploring various directions to improve proof search, such as developing value models to assess the promise of proof goals.¹⁵

Proof search alone does not solve theorem proving, where a fundamental challenge is a discrete, infinite action space. Proof search cannot succeed if the model cannot produce high-quality actions in the first place. In the context of theorem proving, mathematical creativity can manifest as actions exceeding the current model’s capabilities, akin to the “divine move ( )”—a legendary concept in Go. We would not expect to find them if the action space were an infinite, unstructured list. Fortunately, mathematics is structured, making it possible—though still challenging—to find the divine moves. Next, we discuss several ways of leveraging structures in mathematics.

Exploiting hierarchies and learning abstractions.  Theorems build upon smaller lemmas, which in turn break down into even simpler subgoals. Several existing theorem provers leverage this hierarchical structure. Draft, Sketch, and Prove¹¹ transformed informal proofs into formal “proof sketches”—skeletons of formal proofs with “holes,” that is, open goals left unproven, yielding a hierarchical structure. POETRY³⁵ recursively decomposed goals in proof sketches using an LLM. While these works demonstrated the potential of hierarchical decomposition, it is still a significant challenge to decompose realistic high-level goals with current LLMs.

Abstraction is central to human mathematical practice. We first learn natural numbers through counting; years later, those operations show up in solving equations but do not require as much attention anymore. In interactive theorem proving, abstractions can be encapsulated in new definitions, lemmas, and tactics. While most existing methods assume they are predefined and fixed, recent work has explored learning abstractions. For instance, LEGO-Prover³⁷ used LLMs to propose and prove new lemmas, integrating them into its library to help prove further theorems. Lemma mining from existing proof corpora has also been explored.¹² These lemmas, not explicitly factored out by humans, are still useful for automation. On learning tactics, Peano²⁷ has proposed to learn simple proof strategies from an agent’s own solutions to past problems, in a bootstrapping fashion. However, these approaches have so far been limited to simpler formal systems, and it is still an open challenge to synthesize entirely new tactics in full-fledged formal theorem-proving languages like Lean.

Incorporating external knowledge.  Formal mathematical reasoning can benefit from explicitly retrieving and incorporating knowledge from databases of existing lemmas/definitions. ReProver³⁸ and COPRA³² demonstrated performance gains through standard retrievers such as Dense Passage Retrieval.¹³ A promising direction involves developing retrievers tailored to formal math, for example, structured or neurosymbolic retrievers. Another avenue is to grow the knowledge base dynamically. For example, the system could decompose high-level proof goals into subgoals, cache a subset of these subgoals as modules, and use them in subsequent proof efforts. Deciding which subgoals are “interesting” enough to be modularized in this way is a challenge.

Autoformalization.  LLMs can readily generate autoformalization candidates that are usable after human review and refinement. To bootstrap autoformalization from this process, we need a system for collecting and storing human feedback, creating a continuously evolving dataset of synchronized informal and formal knowledge. This dataset will support the midterm goal of robust and faithful translations between informal and formal statements. In the long term, AI-based autoformalization should go beyond direct translation. For example, it should handle implicit assumptions and hand-waived proofs that pose challenges in formalizing mathematics. The model should be capable of inferring missing information and identifying cases where gaps cannot be resolved, necessitating strong reasoning capabilities. Additionally, it should detect and correct errors or inconsistencies by engaging with humans to clarify intent and refine its understanding.

Theorem proving.  Current machine learning methods can assist humans in formal proof development by suggesting useful definitions, lemmas, and proof steps.²⁹ They can also autonomously prove simple theorems and fill small gaps in larger proofs in a domain-general manner.³⁸ A natural next step is advancing toward more complex tasks, such as autonomously contributing to large-scale formalization projects. This requires AI to move beyond individual proofs to decompose larger results, propose new definitions and lemmas, and explore alternatives as the project develops. Evaluating such capabilities may require new benchmarks derived from real-world formalization efforts, incorporating GitHub metadata such as issues and commits. In the long term, we can envision AI systems that not only solve mathematical problems but also discover new mathematics beyond human capabilities. A key challenge will be developing meaningful metrics to track progress toward this open-ended goal, as current evaluations primarily measure proficiency in existing mathematics.

Verified reasoning in natural language.  Existing approaches to incorporate verification into natural language reasoning either rely on neural verifiers, which can be brittle and lack formal guarantees, or attempt to fully formalize the problem,⁴⁰ limiting their applicability. Future models should reason seamlessly across natural language and formal systems such as Lean. By interleaving natural language with formal reasoning, they should selectively determine which parts of reasoning to process using formal systems. Such an approach could enable complex mathematical reasoning and planning in real-world applications that integrate mathematical components with elements that are challenging to formalize, such as common sense and human preferences.

Formal verification and verifiable generation.  Current LLMs still struggle with verifying simple properties of small programs,²⁰ let alone synthesizing formally verified code—a more nascent task for which we do not have a large-scale, high-quality benchmark to evaluate AI models. Therefore, developing benchmarks and methods for small programs is an important goal in the short to mid-term.^31,39 In the long term, AI should be able to verify and synthesize entire projects with complex functional and security properties. This capability requires decomposing large systems into smaller verifiable components, a task currently performed by humans but may be tackled by advanced AI agents capable of planning and problem solving to navigate the intricate dependencies and interactions in large codebases. Additionally, future AI should help users generate, explain, and debug formal specifications interactively.