Bolzano：从专家引导的证明搜索到开放数学问题求解

大型语言模型对数学研究的贡献越来越大，而数学研究的进展往往取决于有效的证明搜索、渐进式改进和仔细验证。我们描述了 Bolzano，一个多Agent开源系统，它使用并行证明者Agent和验证者Agent，并维护人类可读的研究状态。最初手动使用专家选择的问题产生了 8 个结果，其证明由领域专家检查。受这些案例研究的启发，我们在没有针对具体问题的人工指导的情况下对从四组论文中提取的约 3,800 个开放问题运行了 Bolzano，解决了约 200 个开放问题。一项实验使用了理论计算机科学顶级会议 STOC 2026 接受的论文。在那里，我们回答了论文中提出的四个问题，并得到了作者的证实。