From Expert-Guided Proof Search to Automated Open-Problem Solving

AI summary

Overview

Research area: Artificial intelligence for mathematical research — specifically multi-agent LLM systems that search for proofs of open problems in combinatorics and theoretical computer science.

Technical level: Advanced. The system architecture is described in accessible terms, but the mathematical outputs (monotone rank programs, convex quartics, CAT states, planted bicliques) assume graduate-level familiarity with theoretical computer science.

Scope: The paper describes Bolzano, an open-source multi-agent proof-search system, and reports on four automated experiments covering 3,800 extracted open problems plus an earlier expert-guided study of eight problems.

Authors and affiliation: Adrián Zámečník, Matěj Kripner, Martin Koutecký, Martin Balko, Jan Grebík, Pavel Hubáček, Robert Šámal and Václav Rozhoň, from the Computer Science Institute, the Institute of Formal and Applied Linguistics and the Department of Applied Mathematics at Charles University, with one affiliation at the Institute of Mathematics, Czech Academy of Sciences. Published as arXiv:2610.09769v1 [cs.AI] on 07 Oct 2026, under CC BY-SA 4.0.

What This Paper Is About

Large language models are increasingly producing mathematical ideas, but turning those ideas into verified new results requires sustained proof search, iteration and careful checking. The authors build Bolzano, a system in which several "prover" agents attack a problem in parallel while a "verifier" agent critiques their output and maintains a shared, human-readable record of the research so far. The paper's central question is whether this research loop can produce useful mathematics across many open problems without a human choosing and steering each problem individually.

Key Contributions

1. An open-source multi-agent research architecture. Bolzano is an orchestration layer around LLMs in which an "agent" is a model call with a role-specific prompt and supplied research context. The standard pipeline runs sequential research rounds, each consisting of parallel provers, a verifier and a summarizer, over a persistent explicit research state.

2. A persistent, human-readable research state. Each problem task maintains three Markdown documents — notes.md (insights, failed approaches, conjectures, simplified proofs), proofs.md (detailed candidate proofs) and output.md (the current outcome for the researcher) — plus earlier round summaries. Within the automated loop, only the verifier stage may update these documents; provers propose material but do not overwrite the common state, and the summarizer does not write to the three research documents.

3. An end-to-end automated workflow from paper to problem to attempted proof. A separate LLM-based extraction step reads papers, finds explicitly stated open problems, checks whether the source paper itself resolves them, runs a literature search to test whether they are still open, and assembles a self-contained task with definitions, assumptions and related work for Bolzano to attack.

4. A four-experiment evaluation at scale with human and author verification. Four collections totalling 3,800 problems were run autonomously, producing 485 outputs flagged as promising and 214 estimated solved, including four results from STOC 2026 accepted papers that the source authors confirmed in private correspondence in June and July 2026.

Main Findings

• Expert-guided use produced eight verified results. The initial Bolzano study documented eight problems solved with domain-expert checking, with strategic guidance supplied in some cases. Six results were classified as publishable research and five as essentially autonomous under the taxonomy of Feng et al.

• Four large-scale automated experiments covered 3,800 problems. Four paper collections were used: newly released arXiv papers in math.CO and cs.DS; STOC 2026 accepted papers; earlier FOCS, SODA and STOC papers; and work associated with the Midsummer Combinatorial Workshop 2026 and earlier. Problems may overlap between collections.

• Per-collection results (Table 1). The arXiv math.CO/cs.DS collection contained 1,600 problems run on GPT-5.5 for 4 rounds, yielding 250 promising outputs and 90 estimated solved. STOC 2026 contained 420 problems run on GPT-5.5 for 4 rounds, yielding 41 promising outputs and 4 solved. Earlier FOCS/SODA/STOC contained 900 problems run on GPT-5.6 Sol for 2 rounds, yielding 57 promising and 40 estimated solved. The Midsummer Combinatorial Workshop collection contained 880 problems run on GPT-5.6 Sol for 2 rounds, yielding 137 promising and 80 estimated solved. The total was 485 promising and 214 solved.

• 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; author feedback on many results suggests the estimates are reasonable. For STOC 2026, only the four results that were carefully checked and author-verified are reported.

• Planted bicliques. Bolzano found a one-pass algorithm using O(log n) bits of memory to detect a semi-random planted biclique when both sides have size at least Cn^(2/3), matching the known lower bound up to logarithmic factors.

• Monotone rank programs. Bolzano found an exponential separation between monotone rank programs and monotone span programs. For F_m(a,b) = ⋁_{i=1}^{m}(a_i ∧ b_i), there is a monotone span program with 2m rows over every field, while every column-full-rank monotone rank program needs exactly m2^m rows.

• Convex quartics. Bolzano constructed a strongly convex quartic polynomial in two variables with rational coefficients whose zero sublevel set consists of one irrational point, giving a convex quartic feasibility problem that has a solution but no rational witness.

• Biased CAT states. Bolzano proved an Ω(log n) circuit-depth lower bound for both joining two biased CAT states and splitting one into two, including the entropy-balanced case H(α) = 2H(β) that was left open in the source paper.

• Caveat on two of the four confirmations. For the convex quartic and biased CAT state results, the authors of the source papers reviewed only the main idea, not the full proof.

• Verification remains the bottleneck. The verifier is another LLM, not a formal proof checker: an accepted but incorrect lemma may propagate through persistent memory, and later agents may repeat it with increasing confidence. Observed failures include missing assumptions, proofs addressing weaker versions of the original questions, invalid arguments and rediscoveries of known results. Bolzano's documents therefore remain candidate mathematics until checked by a human or formal system.

• Screening is imperfect in both directions. Flagged outputs were selected for human assessment, while outputs not flagged as promising were not systematically reviewed, so unflagged runs cannot all be declared unsolved.

• Stated limitations. The experiments use different problem collections, models and budgets, include no comparison with direct use of the underlying models, and leave comparative efficiency and the final yield of verified solutions to further evaluation. Bolzano's documents also carry no formal proof status.

• Agent constraints. In all reported experiments the prover, verifier and summarizer operated without web search, code execution, direct filesystem access or any tools, in order to evaluate LLMs' pure reasoning capabilities over supplied mathematical text.

Methodology in Plain English

The team built a loop around existing language models rather than training a new one. For a given problem, several "prover" agents are each given the same task description and the same current working documents, plus optional role- or round-specific instructions. They are asked to explore proof strategies, construct examples or counterexamples, prove special cases and identify gaps. They run concurrently and never see each other's responses within a round.

Their outputs are then handed to a "verifier" agent, which assesses the arguments, identifies unjustified steps, reconciles compatible ideas and decides what to retain. The verifier returns a structured response with feedback, blocking issues and proposed append-or-replace edits to the three research documents. The application validates that response's schema before applying the edits.

A separate summarizer then writes a concise account of the round's progress and remaining questions, which is stored for display and later rounds. If the preset round budget remains, the next round begins. A run marked "completed" simply means it finished its allocated rounds — it does not mean the problem was solved.

To go from papers to problems without human selection, the authors used a separate LLM-based extraction workflow built on a general-purpose agent harness with access to local paper files and web search. The agents read papers for explicitly stated problems, checked whether each paper resolved its own problem, and performed a literature search to test whether the problem remained open. Candidates already resolved were excluded, and retained problems were rewritten as self-contained tasks with the necessary definitions, assumptions and related work.

After a run, an LLM postprocessing step reads the output and proof material to identify substantive claims — proofs, counterexamples, algorithms or improved bounds — and a persistent registry flags duplicate packages. Promising claims were compared against the actual source question, including its hypotheses, quantifiers and conventions, and assessed for proof gaps, restricted scope and overlap with known results. The authors note this check matters because a correct proof of an inaccurately extracted statement may not advance the original problem.

Selected candidates were rewritten as mathematical notes and some received a further LLM audit using the note and source text, with the extracted problem treated only as a non-authoritative hint. The audit requires two conditions to pass: the claimed problem must be supported by the source under its intended reading, and the proof must be substantially correct. A failed or unresolved condition produces a negative decision. The audit also produced structured assessments of resolution completeness, scope limitations, issue severity, fixability and review priority, so an audit pass can still describe only substantial partial progress. These records guided closer human inspection and, where available, assessment by the original problem authors. The authors acknowledge that their expertise does not cover all relevant fields and that screening and audit protocols evolved across the experiments.

Why This Matters

The paper argues that the practical value of LLM-driven mathematics may lie less in isolated clever answers and more in a repeatable pipeline: extract open problems from the literature, allocate a fixed research budget to each, keep counterexamples and partial advances as well as complete proofs, and concentrate scarce human attention on the most promising outputs. The four STOC 2026 confirmations are notable because they come from a prime conference for theoretical computer scientists, and some authors plan to include results in revised versions of their papers. At the same time, the paper is explicit that automated verification is the weak link and that its own solved counts (except STOC 2026) are estimates rather than confirmed theorems.

Real-world applications (note: the paper does not report deployed applications; these follow from the pipeline it describes):

• Automated literature triage, where open problems and conjectures in new preprints are extracted and checked for whether they have already been settled.
• Human-in-the-loop research assistance, in which the readable notes.md/proofs.md/output.md state lets a mathematician resume, correct or redirect a machine's proof attempt.
• Building blocks for formal verification pipelines, since the authors position Bolzano's documents as candidates awaiting a human or formal checker.
• Benchmarking and evaluation of reasoning models on research-level mathematics rather than competition-style problems.

Industry relevance: The architecture is an orchestration layer around existing models, not a new model, which makes it directly relevant to teams building multi-agent systems with persistent shared state, structured verifier feedback and duplicate-detection registries. The paper's failure modes — schema-validated but wrong outputs, confidently propagated incorrect lemmas, and claims that quietly address a weaker version of the original question — are general problems for any agentic pipeline whose outputs feed forward into later steps.

Future Directions

• Making verification reliable. The verifier is an LLM, and the authors note an accepted but incorrect lemma can propagate through persistent memory with increasing confidence. Connecting Bolzano to formal proof checkers, or designing verification that resists this drift, is the most direct open problem.

• Better screening in both directions. Because unflagged outputs were not systematically reviewed, the true number of solved problems is unknown; the authors state that screening can miss useful output. Improving candidate detection would sharpen any future yield estimate.

• Controlled comparison against the underlying models. The paper explicitly includes no comparison with direct use of GPT-5.5 or GPT-5.6 Sol, and the experiments used different collections, models and budgets. Isolating the contribution of parallel provers, verifier critique and persistent state is left open.

• Scaling and calibration of budgets. Each run was given a fixed number of rounds (4 for the GPT-5.5 collections, 2 for the GPT-5.6 Sol collections). Whether more rounds, more provers or tool access (web search, code execution) improve yield at acceptable cost is untested here.

• Broader author validation. Only four results were carefully checked and confirmed by source authors, and for two of them the authors reviewed only the main idea rather than the full proof. Extending rigorous author review to more of the 485 promising outputs would test the pipeline's real productivity.

Target Audience

This paper is aimed at AI researchers working on multi-agent systems, LLM reasoning and automated theorem discovery; theoretical computer scientists and mathematicians curious about machine-generated contributions to their fields; and engineers building agentic research or literature-analysis pipelines who want a concrete, open-source reference architecture with reports of real failure modes. Readers seeking rigorous, formally verified mathematical results will find the paper's own framing — candidate mathematics pending human or formal checking — essential context.

Authors’ abstract

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.