# Bolzano: Case Studies in LLM-Assisted Mathematical Research

arXiv: https://arxiv.org/abs/2604.16989 · HTML: https://mlsanity.com/paper/2604.16989/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 11 of its 50 references that are in the map.
- First posted on arXiv 18 Apr 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 11 of 11)

- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Improving Factuality and Reasoning in Language Models through Multiagent Debate](https://mlsanity.com/paper/2305.14325/) (2023)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [Right Is Not Enough: The Pitfalls of Outcome Supervision in Training LLMs for Math Reasoning](https://mlsanity.com/paper/2506.06877/) (2025)
- [Universal Optimality of Dijkstra via Beyond-Worst-Case Heaps](https://mlsanity.com/paper/2311.11793/) (2023)
- [Opinion Diffusion and Campaigning on Society Graphs](https://mlsanity.com/paper/2010.00651/) (2020)
- [Selection and Influence in Cultural Dynamics](https://mlsanity.com/paper/1304.7468/) (2013)

## Built on by (most cited first, 3 of 3)

- [Using large language models to probe the limits of atom-centered structural descriptors](https://mlsanity.com/paper/2607.26984/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving](https://mlsanity.com/paper/2610.09769/) (2026)

## Abstract (arXiv)

We report new results on eight problems in mathematics and theoretical computer science, produced with the assistance of Bolzano, an open-source multi-agent LLM system. Bolzano orchestrates rounds of interaction between parallel prover agents and a verifier agent while maintaining a persistent knowledge base that is carried across rounds. Classified using the significance-autonomy taxonomy of Feng et al., six of the eight results reach the level of publishable research, and five of the eight were produced essentially autonomously by Bolzano. Our results provide evidence that LLMs can contribute meaningfully to mathematical research, complementing recent reports by Bubeck et al., Woodruff et al., and others.