Source-linked AI summary
From Expert-Guided Proof Search to Automated Open-Problem Solving
Adrián Zámečník, Matěj Kripner, Martin Koutecký, Martin Balko, Jan Grebík, Pavel Hubáček, Robert Šámal, Václav Rozhoň
TL;DR
Open research questions require efficient proof search, incremental progress and careful verification. Bolzano combines parallel prover agents, verifier feedback and a persistent research state, then tests automated problem extraction and search across papers. The experiments report a few hundred solutions from 3,800 attempts, while candidate outputs still require human or formal checking.
Problem
The paper asks whether automated problem extraction and proof search can produce mathematical results across open questions without problem-specific human steering.
Source: §1 · pp. 1–2Method
Bolzano combines parallel LLM proof exploration, verifier feedback and a persistent shared research state in a multi-agent workflow.
Source: §2 · p. 2Results
Across four automated experiments, Bolzano found a few hundred solutions in 3,800 attempts, including four confirmed results from STOC 2026 papers.
Source: §1 · p. 1Takeaways & Limitations
Abstract
from arXiv · showhide
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.
1 Introduction
Bolzano investigates whether automated extraction and proof search can turn research-paper questions into mathematical results without problem-specific human steering. The study builds on expert-checked case studies and reports results across combinatorics and theoretical computer science.
1 Introduction
- Recent mathematical milestones include a disproof of the Erdős unit-distance conjecture checked and refined by mathematicians and other reported advances.These developments motivate systems for sustained proof search and mathematical research.Source: §1 · p. 1
- Four automated experiments applied Bolzano to 3,800 attempts and found a few hundred solutions, including four confirmed results from STOC 2026 papers.The introduction says some source-paper authors plan to include results in revised versions of their papers.Source: §1 · p. 1
- Earlier expert-guided use produced eight problems whose proofs were checked by domain experts, motivating tests without individual human steering.Bolzano’s initial study helped motivate the broader automated experiments.Source: §1 · p. 1
- The study examines how automated problem extraction and proof search can produce mathematical results across combinatorics and theoretical computer science.It describes the workflow from problem extraction through human review.Source: §1 · p. 2
- Bolzano’s iterative architecture resembles Aletheia’s proof generation, verification and revision, while also using parallel informal proof generation and a persistent shared knowledge base.The passage also contrasts it with AlphaEvolve [10] and describes Feng et al.’s [8] human evaluation of open Erdős problems.Source: §1 · p. 2
2 Bolzano’s research loop
Bolzano runs parallel proof exploration, verifier critique and shared research notes in successive rounds. Its verifier is an LLM rather than a formal proof checker, so candidate mathematics requires further checking.
2 Bolzano’s research loop
- Bolzano’s standard pipeline runs sequential research rounds with parallel provers, a verifier and a summarizer.It is an open-source orchestration layer around LLMs.Source: §2 · p. 2
- Three Markdown documents preserve insights and failed approaches, candidate proofs, and the current outcome, giving later rounds a concise record of prior work.Earlier round summaries also enter the state, allowing agents to build on earlier ideas without reading every response.Source: §2 · p. 2
- Provers work concurrently from the same task and current documents, exploring strategies, examples, counterexamples, special cases and proof gaps.They do not see one another’s current-round responses, and their approaches need not be independent.Source: §2 · p. 2
- The verifier assesses prover arguments and proposes document updates; it alone updates shared documents within the automated loop.The application validates the verifier’s structured response and applies its append or replace operations.Source: §2 · p. 2
- A separate summarizer records progress and remaining questions, while automated experiments provide no problem-specific human guidance during solving.A run marked completed has only finished its allocated rounds, not necessarily solved the problem.Source: §2 · p. 2
- Because the verifier is an LLM rather than a formal checker, an incorrect accepted lemma may propagate and be repeated with increasing confidence.Bolzano’s documents remain candidate mathematics until checked by a human or formal system.Source: §2 · pp. 2–3
3 Initial use with domain experts
Initial expert-guided use of Bolzano yielded eight problems with proofs checked by domain experts. These cases motivated a scalable workflow that retains partial advances and directs human attention to promising outputs.
3 Initial use with domain experts
- Eight problems were solved by Bolzano and their proofs were checked by domain experts, with strategic guidance supplied in some cases.The initial report classifies six results as publishable research and five as essentially autonomous under Feng et al.’s [7] taxonomy; autonomy concerns argument generation after human problem preparation.Source: §3 · p. 3
- The proposed scalable workflow allocates each problem a fixed research budget, retains partial advances as well as complete proofs, and focuses human attention on promising outputs.Source: §3 · p. 3
4 Four automated experiments
Bolzano was run on open problems extracted from four paper collections, with no problem-specific human instructions during solving. In the STOC 2026 experiment, authors confirmed four selected results.
4 Four automated experiments
- The experiments covered four paper collections; an LLM-based workflow extracted open problems, checked whether they remained unresolved, and assembled self-contained tasks.Collections included new arXiv papers, STOC 2026 papers, earlier conference papers, and workshop-associated work.Source: §4 · p. 3
- Each collection had a specified model and round configuration, with one prover at maximum available reasoning effort; records included tasks, outputs, proof details, and sometimes notes and source papers.Source: §4 · p. 3, Table 1 · p. 3
- Promising outputs were checked against source questions and proof gaps, then audited for source support and substantial correctness; solved counts outside STOC 2026 are estimates.Unflagged outputs were not systematically reviewed.Source: §4 · pp. 3–4
4.1 Four results from STOC 2026
- Authors of the source papers confirmed four selected results from the STOC 2026 experiment.The confirmations were in private correspondence in June and July 2026.Source: §4.1 · p. 4
- Bolzano found a one-pass O(log n)-bit algorithm for detecting semi-random planted bicliques when both sides have size at least Cn2/3, matching the known lower bound up to logarithmic factors.Source: §4.1 · p. 4
- Bolzano proved an exponential separation: span programs use 2m rows over every field, while column-full-rank monotone rank programs need exactly m2^m rows.The result concerns F_m(a, b) described in the source passage.Source: §4.1 · p. 4
- Bolzano constructed a strongly convex rational-coefficient quartic in two variables whose zero sublevel set is one irrational point, giving a feasible problem with no rational witness.Source: §4.1 · p. 4
- Bolzano proved an Ω(log n) circuit-depth lower bound for joining or splitting biased CAT states, including the source paper’s open entropy-balanced case.The case satisfies H(α) = 2H(β).Source: §4.1 · p. 4
5 Discussion
Bolzano connects parallel proof exploration to a persistent research record for human-steered and unattended runs. The experiments reveal assessment challenges and leave comparative efficiency and verified-solution yield for further evaluation.
5 Discussion
- Bolzano connects parallel proof exploration to a persistent research record that supports both human steering and unattended runs.Source: §5 · p. 4
- Observed failures included missing assumptions, arguments for weaker versions of questions, invalid proofs, and rediscoveries of known results.Source: §5 · p. 4
- Different collections, models, and budgets, plus no comparison with direct model use, leave comparative efficiency and final verified-solution yield for further evaluation.Source: §5 · p. 4
- For the convex quartic and biased CAT results, source-paper authors reviewed only the main idea, not the full proof.Source: §5 · p. 4