Summary (Overview)

• Bolzano is an open-source, multi-agent system for mathematical proof search that uses parallel prover agents, a verifier agent, and a persistent human-readable research state (notes, proofs, output documents) to enable sustained, iterative problem-solving.
• Initial expert-guided use on eight selected problems produced results verified by domain experts, with six classified as publishable research and five as essentially autonomous.
• Four large-scale automated experiments were run on ~3,800 open problems extracted from arXiv preprints (math.CO, cs.DS), STOC 2026 accepted papers, earlier FOCS/SODA/STOC papers, and Midsummer Combinatorial Workshop papers — solving 214 problems in total (485 flagged as promising).
• Four confirmed results came from STOC 2026 papers, verified by the original authors, including a memory-optimal planted biclique detection algorithm and an exponential separation between monotone rank programs and monotone span programs.
• The system's key bottleneck is human/LLM verification: distinguishing correct, novel results from invalid arguments, weaker restatements, and rediscoveries of known theorems.

---

Introduction and Theoretical Foundation

Large language models (LLMs) are increasingly contributing to mathematical research beyond competition benchmarks. Notable milestones include:

• Early GPT-5 and Gemini case studies providing proof ideas, counterexamples, and extensions [4, 14].
• A disproof of the Erdős unit-distance conjecture, checked and refined by mathematicians [1].
• A collection of advances across mathematics and theoretical computer science [11].
• A reported lower bound exceeding two-thirds for the proportion of zeta zeros that are simple and on the critical line [6].

Bolzano [2, 3] builds on these developments by organizing sustained proof search through parallel informal proof exploration, critique, and shared mathematical notes. The central research question motivating this paper is: Can the same research loop produce useful mathematics across many open problems without individual human steering?

Related systems:

• Aletheia [7]: iterative framework for natural-language proof generation, verification, and revision.
• AlphaEvolve [10]: combines evolutionary program search with executable evaluation.
• Feng et al. [8]: automated attempts on open Erdős problems with human evaluation.

Bolzano's architecture differs by combining parallel informal proof generation with verifier feedback and a persistent shared knowledge base, supporting both expert-guided and autonomous investigations.

---

Methodology

2.1 Research Loop Architecture

The standard pipeline runs sequential research rounds, each consisting of:

1. Parallel provers — explore proof strategies, construct examples/counterexamples, prove special cases, identify gaps.
2. A verifier — assesses arguments, identifies unjustified steps, reconciles compatible ideas, and updates the shared state.
3. A summarizer — produces a concise account of round progress and remaining questions.

Explicit research state — three Markdown documents persist across rounds:

• notes.md: insights, failed approaches, conjectures, simplified proofs.
• proofs.md: detailed candidate proofs.
• output.md: current outcome for the researcher.

Agent constraints — In all experiments, agents operated without web search, code execution, or tools; the research state was included in prompts. This isolates LLMs' pure reasoning capabilities over supplied mathematical text.

Verification scope — The verifier is another LLM, not a formal proof checker. Accepted-but-incorrect lemmas may propagate through persistent memory, so documents remain candidate mathematics until human or formal verification.

2.2 Automated Problem Extraction

A separate LLM-based workflow:

1. Identifies explicitly stated open problems, questions, and conjectures in collected papers.
2. Checks whether the paper itself resolves the problem.
3. Performs a literature search to confirm the problem remains open.
4. Assembles self-contained tasks with necessary definitions, assumptions, and related work.

2.3 Screening and Audit

• LLM postprocessing reads outputs to identify substantive claims (proofs, counterexamples, algorithms, improved bounds).
• Source checks compare claims against the actual source question (hypotheses, quantifiers, conventions) and assess proof gaps, restricted scope, and overlap with known results.
• Structured audit requires two conditions: (1) the claimed problem is supported by the source, and (2) the proof is substantially correct. A failed condition yields a negative decision.

---

Empirical Validation / Results

3.1 Initial Expert-Guided Results

The initial Bolzano report [2] documents eight problems solved and checked by domain experts, with six classified as publishable research and five as essentially autonomous under the taxonomy of Feng et al. [7].

3.2 Four Automated Experiments

Table 1: Automated experiments (different collections use different configurations; all runs used one prover set to maximum reasoning effort):

¹Promising = flagged by LLM postprocessing as substantive claims. ²Solved = confirmed by structured audit and/or author verification.

3.3 Four Confirmed STOC 2026 Results

Authors confirmed these results in private correspondence in June and July 2026:

1. Planted bicliques [9]: A one-pass algorithm using $O(\log n)$ bits of memory detects a semi-random planted biclique when both sides have size at least $C n^{2/3}$. This matches the known lower bound up to logarithmic factors.

2. Monotone rank programs [5, Section 1.3]: An exponential separation between monotone rank programs and monotone span programs. For

$$F_m(a, b) = \bigvee_{i=1}^{m} (a_i \wedge b_i),$$

there is a monotone span program with $2m$ rows over every field, while every column-full-rank monotone rank program needs exactly $m 2^m$ rows.

3. Convex quartics [13]: A strongly convex quartic polynomial in two variables with rational coefficients whose zero sublevel set consists of one irrational point. This yields a convex quartic feasibility problem with a solution but no rational witness.

4. Biased CAT states [12]: An $\Omega(\log n)$ circuit-depth lower bound for both joining two biased CAT states and splitting one into two, including the entropy-balanced case $H(\alpha) = 2H(\beta)$ left open in the source paper.

---

Theoretical and Practical Implications

Theoretical significance:

• Demonstrates that LLM-based systems can move beyond competition problems to open research questions in combinatorics and theoretical computer science.
• The planted biclique result matches known lower bounds up to logarithmic factors, showing LLM-discovered algorithms can be information-theoretically optimal.
• The convex quartic result highlights subtle issues in rational witness existence for convex optimization.
• The monotone rank program separation resolves a structural question about computational models' relative power.

Practical implications:

• The automated pipeline can process thousands of problems with minimal human intervention, transforming open questions from papers into candidate results.
• The main bottleneck shifts from generation to verification: distinguishing correct novel results from invalid arguments, weaker restatements, and rediscoveries.
• Observed failure modes include: missing assumptions, proofs of weaker versions, invalid arguments, and rediscovery of known results.
• Screening can miss useful output, so unflagged runs cannot be declared unsolved — human oversight remains essential.

---

Conclusion

Bolzano connects parallel proof exploration to a persistent research record that supports both human steering and unattended runs. The manually checked case studies establish the workflow's research value, and the four automated experiments extend its reach to ~3,800 problems, yielding 214 solved and four author-confirmed results from STOC 2026 papers.

Key limitations:

• Experiments use different problem collections, models, and budgets with no comparison to direct use of underlying models.
• The comparative efficiency and final yield of verified solutions require further evaluation.
• The verifier is an LLM, not a formal checker — human assessment of correctness, scope, and novelty remains the critical bottleneck.

Future directions: The authors suggest that improving automated verification and screening protocols, as well as more systematic comparisons with baseline model usage, are natural next steps for advancing LLM-based mathematical research systems.