This assessment is based on version 1 of this paper. Version 2 is now available on arXiv — the authors may have revised their methods, results, or conclusions.
Advancing Mathematics Research with AI-Driven Formal Proof Search
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala
Abstract
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
AI Impact Assessments
(1 model)Scientific Impact Assessment: "Advancing Mathematics Research with AI-Driven Formal Proof Search"
1. Core Contribution
This paper presents AlphaProof Nexus, a framework for LLM-aided formal proof generation in Lean, and demonstrates its ability to autonomously solve open research-level mathematical problems. The headline results are striking: 9 of 353 open Erdős problems resolved (including problems open for 56 years), 44/492 OEIS conjectures proved, a 15-year-old question in algebraic geometry settled, and an improved convergence bound in convex optimization discovered. The key conceptual contribution is shifting formal AI theorem proving from competition mathematics and human-aided formalization toward autonomous discovery on genuine research problems.
The system architecture spans four agent configurations: (A) a basic Ralph-loop agent with Lean compiler feedback, (B) adding AlphaProof as a subgoal solver, (C) adding evolutionary population-based search with Elo-rated sketches, and (D) the full-featured combination. The evolutionary component is notable for addressing the mismatch between binary proof verification and the graduated fitness landscapes evolutionary algorithms typically require, solved via LLM-based relative sketch ranking aggregated into Elo scores.
2. Methodological Rigor
The evaluation methodology has several strengths. The Erdős problem set was determined by what the community had formalized (353 problems), avoiding cherry-picking. Expert validation confirmed formalizations faithfully captured original conjectures. All Lean proofs are publicly released, providing reproducibility at the verification level.
The agent comparison study is well-designed: 100 independent runs for simpler agents allow statistical analysis via chunking, while cost-normalized comparisons across architectures provide meaningful head-to-head evaluation. The use of USD as a common cost currency is pragmatic and informative.
However, some limitations exist. The post-hoc nature of the architecture comparison is acknowledged but important — the basic agent's success was tested only on the 9 problems the full agent solved, not on the full 353. The OEIS evaluation involved Gemini-based problem selection and autoformalization, introducing potential selection bias toward problems amenable to the system. The paper does not report confidence intervals for Agent (D) results due to computational constraints. AlphaProof's cost (~$60/problem) is excluded from reported costs, which slightly complicates interpretation.
3. Potential Impact
Mathematics: This work demonstrates a viable workflow where AI generates formally verified proofs of open problems, with mathematicians providing problem formulations and validating that formalizations match informal statements. The detection of misformalizations (Erdős #125, #741) is a particularly valuable secondary capability. The proof sketches, even when incomplete, helped collaborators understand problems — suggesting utility beyond just solving.
AI for Science: The finding that the basic agent could replicate all 9 Erdős successes (though at higher cost on harder problems) is perhaps the most consequential architectural insight. It suggests that as frontier LLMs improve, simpler agentic loops may suffice, potentially democratizing this capability. This aligns with broader trends in AI where simple approaches with strong base models outperform complex engineered systems.
Formal Verification: The work validates the paradigm of using formal languages as a medium for mathematical discovery (not just verification), distinguishing it from natural-language proof systems that require expert review.
4. Timeliness & Relevance
This paper arrives at a critical juncture. Recent work (Aletheia, OpenAI's systems) has shown LLMs solving Erdős problems informally, but the reliability question remained. Formal verification addresses this directly. The paper explicitly positions itself against the concurrent informal approaches and makes a compelling case that formal proof search filters out hallucinations that plague natural-language systems — a point vividly illustrated by the failure analysis showing agents hallucinating "established results."
The timing also captures an interesting snapshot of a moving target: the basic agent's surprising competitiveness reflects rapid LLM improvement, and the paper honestly acknowledges that the full-featured agent's advantages may diminish over time.
5. Strengths & Limitations
Key Strengths:
Notable Limitations:
Additional Observations:
The deformalized proofs in the supplementary material are themselves interesting mathematical contributions. The Erdős #12 construction using CRT and 3-AP-avoiding sets, and the Hilbert function log-concavity proof, demonstrate genuine mathematical sophistication. The optimization result, where the agent simultaneously discovered a novel parameter schedule and its proof, points toward a particularly promising use case.
The paper represents a significant milestone in AI-assisted mathematics, though it is important to note that the problems solved, while genuinely open, are not among the hardest open problems in mathematics. The concentration in combinatorics and number theory reflects both Mathlib coverage and the nature of problems amenable to constructive proof strategies.
Generated May 22, 2026
Comparison History (25)
Paper 2 demonstrates a major milestone: AI autonomously solving previously open mathematical problems (Erdős problems) using formal proof search. This represents a significant breakthrough in AI-driven scientific discovery with immediate, tangible impacts across multiple fields of mathematics and theoretical physics. While Paper 1 provides valuable theoretical insights into RLHF failure modes, Paper 2's practical demonstration of advancing human knowledge in mathematics gives it a higher potential breadth and magnitude of scientific impact.
Paper 2 demonstrates AI solving genuinely open mathematical problems (9 Erdős problems, 44 OEIS conjectures) for the first time at scale, representing a landmark achievement at the intersection of AI and mathematics research. This has profound implications for how mathematical research is conducted and establishes a new paradigm of AI-assisted theorem proving with verified correctness. While Paper 1 makes solid contributions to LLM inference efficiency with practical speedups, context sparsity is an incremental optimization. Paper 2's impact spans mathematics, formal verification, and AI, with immediate real-world deployment in active research.
Paper 2 demonstrates AI solving genuinely open mathematical problems (9 Erdős problems, 44 OEIS conjectures) with formal verification, representing a landmark achievement in AI-for-mathematics. This has transformative implications for mathematical research methodology and is already being deployed across multiple mathematical subfields. While Paper 1 presents a solid engineering contribution for optimizing agent skills with impressive benchmarks, it is ultimately an incremental advance in prompt/skill optimization. Paper 2's direct scientific discoveries and paradigm-shifting potential for mathematics research give it substantially higher impact.
Paper 2 likely has higher impact: it introduces a novel IDS paradigm that jointly synthesizes implementations and proofs with learning from failures, and demonstrates strong, complete benchmark gains (7/7) with low cost/time plus performance optimization. The real-world applications (formally verified distributed systems) are immediate and broadly relevant to safety-critical software engineering and industry, spanning PL, formal methods, systems, and AI. Paper 1 is timely and exciting for mathematics, but its demonstrated scope (solving a small fraction of open problems) suggests narrower near-term practical impact than verified-systems automation.
Paper 1 introduces a foundation model at an unprecedented scale (5 million participants) for wearable health data. Its impact on personalized medicine, predictive health, and direct societal well-being is massive. While Paper 2 demonstrates a profound breakthrough in AI reasoning for pure mathematics, Paper 1's real-world applications across numerous medical domains, combined with clinician-validated agents, offer a broader and more immediate translational scientific impact.
Paper 1 likely has higher scientific impact due to greater novelty and cross-field breadth: it demonstrates AI-driven formal proof search solving previously open mathematical problems, a qualitatively new capability with implications for mathematics, verification, AI alignment/robustness, and scientific discovery workflows. Its methodology (formal verification in Lean, large-scale evaluation on open-problem sets) supports rigor and reproducibility. Paper 2 is highly impactful industrially and timely for recommender systems, but the ideas (multimodal codes, ID-free ranking, warmup training) are more incremental within applied ML and are narrower in academic breadth despite strong scale and deployment results.
Paper 2 demonstrates a groundbreaking methodological leap by using AI to autonomously solve open mathematical problems, including 9 Erdős conjectures. Its use of formal verification (Lean) ensures rigorous correctness, solving a major challenge in AI reasoning. Furthermore, its immediate deployment across diverse fields like algebraic geometry and quantum optics indicates profound and broad scientific impact. In contrast, while Paper 1 offers timely qualitative insights into organizational behavior, its small sample size (24 interviews) and restricted scope limit its transformative scientific potential compared to Paper 2's concrete contributions to fundamental mathematics.
Paper 2 demonstrates a groundbreaking application of LLMs to solve open mathematical problems (including 9 Erdős problems), representing a concrete, verifiable advance in mathematical research. Its impact spans multiple mathematical subfields and establishes a new paradigm for AI-assisted theorem proving. While Paper 1 provides a useful taxonomy and survey of AI sycophancy—an important conceptual contribution—Paper 2's demonstrated ability to solve previously unsolved problems represents a more transformative scientific contribution with immediate, measurable real-world impact on mathematics research.
Paper 1 has higher potential impact due to stronger novelty (large-scale evaluation of LLM+formal verification on open math problems), clear methodological rigor via Lean-verified proofs, and broad cross-field implications (mathematics, AI, formal methods, and downstream scientific domains). Solving open Erdős problems and OEIS conjectures provides high-visibility milestones and strong timeliness amid rapid progress in LLMs. Paper 2 is applied and useful, but its approach (PPO over dispatching-rule selection) is incremental within established DRL scheduling literature and likely narrower in breadth and scientific reach.
Paper 1 likely has higher scientific impact due to a broadly applicable, engineered knowledge infrastructure that measurably improves agentic use of process-based simulators, with strong real-world relevance to climate risk and resource management. Its demonstrated generalization across 119 models and 14 Earth-science domains suggests wide cross-disciplinary utility and infrastructure-like adoption potential. Paper 2 is highly novel and timely for AI+math, but its direct applicability is narrower (specialist formalization workflows) and impact may be constrained by tooling and domain formalization overhead, despite impressive open-problem results.