arXiv cs.CL· 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}·· 10 天前AI 评分71
Bolzano：多智能体系统自动求解约 200 个开放数学问题
Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving
AI 导读
论文提出 Bolzano，一个开源多智能体系统，由并行证明智能体配合验证智能体，并维护人类可读的研究状态。在专家选定问题上的初步人工使用产出 8 个经领域专家核验的证明；随后在无问题特定人工引导下，对从四组论文中提取的约 3800 个开放问题运行，解出约 200 个。
正文 · 原文
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.
| Comments: | Accepted at the 6th Workshop on Mathematical Reasoning and AI (MATH-AI), NeurIPS 2026 |
| Subjects: | Artificial Intelligence (cs.AI); Computation and Language (cs.CL) |
| Cite as: | arXiv:2610.09769 [cs.AI] |
| (or arXiv:2610.09769v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.09769 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Matěj Kripner [view email]
[v1]
Wed, 7 Oct 2026 09:52:46 UTC (13 KB)
来源：arXiv cs.CL · arxiv.org