From Expert-Guided Proof Search to Automated Open-Problem Solving
Authors: Adrián Zámečník, Matěj Kripner, Martin Koutecký, Martin Balko, Jan Grebík, Pavel Hubáček, Robert Šámal, Václav Rozhoň
Organizations: Computer Science Institute, Charles University · Institute of Formal and Applied Linguistics, Charles University · Department of Applied Mathematics, Charles University · Institute of Mathematics, Czech Academy of Sciences
Large language models are increasingly contributing to mathematical research, where progress often depends on efficient proof search, incremental improvements and careful verification. We describe Bolzano, a multi-agent open-source system that uses parallel prover agents with a verifier agent and maintains a human-readable research state. Initial manual use on expert-selected problems yielded 8 results whose proofs were checked by domain experts. Motivated by these case studies, we ran Bolzano without problem-specific human guidance on about 3,800 open problems extracted from four sets of papers, solving about 200 open problems. One experiment used papers accepted to STOC 2026, a top conference in theoretical computer science. There, we answered four questions raised in the papers, as confirmed by their authors.
Figures & tables
Collection
Problems
Model
Rounds
Promising 1 1 1 Outputs flagged by Bolzano as candidate resolutions and selected for human assessment of correctness and relevance to the source question. Outputs not flagged as promising were not systematically reviewed.
Solved 2 2 2 Except for STOC 2026, the solved counts are estimates. These estimates are partially informed by LLM-based assessments of whether the output addresses the source question and whether its argument is substantially correct. We received feedback from authors on many of the results, which suggests that these estimates are reasonable. For STOC 2026, we report only the four results that we checked carefully and that authors of the source papers verified.
arXiv: math.CO , cs.DS
1,600
GPT-5.5
4
250
90
STOC 2026
420
GPT-5.5
4
41
4
Earlier FOCS/SODA/STOC
900
GPT-5.6 Sol
2
57
40
Midsummer Combinatorial Workshop
880
GPT-5.6 Sol
2
137
80
Total
3,800
–
–
485
214
Table 1: Automated experiments. Different collections use different run configurations. All problem runs used only one prover set to maximum reasoning effort available for the model.
We report new results on eight problems in mathematics and theoretical computer science, produced with the assistance of Bolzano, an open-source multi-agent LLM system. Bolzano orchestrates rounds of interaction between parallel prover agents and a verifier agent while maintaining a persistent knowledge base that is carried across rounds. Classified using the significance-autonomy taxonomy of Feng et al., six of the eight results reach the level of publishable research, and five of the eight were produced essentially autonomously by Bolzano. Our results provide evidence that LLMs can contribute meaningfully to mathematical research, complementing recent reports by Bubeck et al., Woodruff et al., and others.
Martin Balko, Jan Grebík, Pavel Hubáček +5
Department of Applied Mathematics, Charles University · Computer Science Institute, Charles University · Institute of Mathematics, Czech Academy of Sciences +1
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.
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18
Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tailored to real-world mathematical practice. To this end, we introduce ProofCouncil, a mathematical agent that is designed to tackle open problems using an author-critic architecture. ProofCouncil served as a submission to the second batch of FirstProof, a challenge consisting of 10 real-world mathematical problems that agents must solve autonomously. Its submissions for 6 of the 10 problems were judged by the referees to be correct up to at most minor revisions, showing the best performance among participating teams. We also evaluate ProofCouncil on 30 open problems collected from mathematical researchers. Among the 21 solutions that received human feedback, 5 were judged completely correct, 2 more were judged promising pending final verification, and a further 8 contained useful partial progress. In this short paper, we describe the development of ProofCouncil and the agent-building library used to create it, which we release as open source to the community.
Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck +4
ETH Zurich · Aarhus University · Independent Researcher +1