Bolzano: Streamlining Automated Proof Search with Parallel Agents

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

Authors: Adri'an Z'ame\v{c}n'ik, Mat\v{e}j Kripner, Martin Kouteck'y, Martin Balko, Jan Greb'ik, Pavel Hub'a\v{c}ek, Robert \v{S}'amal, V'aclav Rozho\v{n}

Executive Summary

Recent research highlights the growing role of large language models in mathematical research, particularly in the areas of proof search and verification. The study introduces Bolzano, an open-source system designed to enhance this process through the use of multiple parallel agents. These agents work together to explore mathematical problems, with one dedicated to verifying the results produced by the others. A key feature of Bolzano is its ability to maintain a clear and accessible record of its research state, making the process more transparent and easier to follow.

The research demonstrates Bolzano's initial effectiveness through manual application on a selection of expert-chosen problems. In these trials, Bolzano generated eight results that were subsequently verified by domain experts, indicating its potential reliability in producing valid mathematical proofs.

Building on these initial findings, the team conducted a more extensive evaluation of Bolzano without relying on human guidance. They applied the system to approximately 3,800 open problems drawn from a variety of academic papers, successfully solving around 200 of these problems. Notably, one segment of their research involved analyzing papers accepted at the upcoming STOC 2026 conference, a prestigious venue for theoretical computer science. In this specific experiment, Bolzano addressed four questions posed in those papers, with validation from the original authors confirming the accuracy of its responses.

The implications of this research are significant for the mathematical community and related fields. Bolzano's ability to autonomously tackle open problems suggests that such systems might streamline the research process, enabling mathematicians to focus on higher-level conceptual work rather than getting bogged down in proof verification. This could lead to faster discoveries and a more efficient approach to resolving long-standing mathematical questions.

However, it is important to note that the results reported stem from benchmark tests and simulations rather than real-world application, meaning that while the findings are promising, further validation in practical settings will be essential to fully understand the system's capabilities and limitations. The transition from controlled experimental use to broader application in real-world scenarios will determine Bolzano's ultimate impact on mathematical research.

Academic 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.