HackerPapers

arXiv:2605.22763cs.AI

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, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri

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.

arXiv comments
Journal reference
DOI
Subjects
cs.AIArtificial Intelligence

On Hacker News

Linked by 3 identifiable commenters in 3 comments across 3 threads, from May 2026 to Aug 2026. Found in 5 HN submissions from May 2026 to Oct 2026. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments3 threads

  1. Ten advances in mathematics and theoretical computer science 1 comment

    • Yes, here is another example of major work in this area: https://arxiv.org/html/2605.22763v1 > 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

      brighteyesView on HNParent context

  2. An OpenAI model has disproved a central conjecture in discrete geometry 1 comment

    • No, problem #326, you didn't give a few days timeline. Google released a paper about solving 9 more Erdos problems for an average of $100 each: https://arxiv.org/html/2605.22763v1 In a year I think we'll probably have seen hundreds of open problems solved, even if there is some…

      cmaView on HNParent context

  3. AlphaProof Nexus solves 9 Erdős problems and proves 44 sequence conjectures 1 comment

    • Link to the "Advancing Mathematics Research with AI-Driven Formal Proof Search" paper that the article references: https://arxiv.org/html/2605.22763v1

      hackernjView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.