Bolzano system solves hundreds of open math problems automatically
From Expert-Guided Proof Search to Automated Open-Problem Solving
Artificial IntelligenceComputation and Language
Summary
Finding mathematical proofs can be very tricky and usually requires expert knowledge. The authors built Bolzano, a system where multiple automated proof solvers work together, checking each other's results and recording progress understandably. Initially, experts guided the system to solve some tough problems and confirmed the proofs. Later, Bolzano worked on thousands of open problems without human hints and solved around 200, including some from top computer science papers confirmed by the original authors.
What this means in practice
- •For mathematical software developers: Integrate Bolzano's multi-agent proof search to automate solving and verifying complex conjectures within mathematical software.
- •For computer science research teams: Use Bolzano to automatically answer open theoretical questions from cutting-edge research papers, accelerating the verification of novel results.
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ň
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.