从专家指导的证明搜索到自动化开放问题求解

大语言模型正日益助力数学研究，而这一领域的进展往往依赖于高效的证明搜索、渐进式改进和严谨的验证。我们介绍了 Bolzano，这是一个开源多智能体系统，使用多个并行的证明智能体与一个验证智能体协作，并维护人类可读的研究状态。最初，通过人工操作该系统处理专家选定的问题，得到了 8 项结果，其证明均经领域专家核验。受这些案例研究启发，我们在没有针对具体问题的人类指导的情况下，让 Bolzano 处理从四组论文中提取的约 3,800 个开放问题，解决了其中约 200 个问题。一项实验使用了理论计算机科学顶级会议 STOC 2026 接收的论文。在该实验中，我们回答了这些论文提出的四个问题，并得到了论文作者的确认。