在现有的基于大型语言模型（LLM）的定理证明器中，虽然它们在形式数学基准测试上取得了显著成果，但仍局限于作为自主代理来证明给定命题。本文提出了 MathCoPilot，这是一种人机协同的系统，体现了数学研究的新范式，在这个框架中，数学家主导高层次的数学方向，而 AI 代理在持续的人类指导下执行详细的形式化和证明工作。
MathCoPilot 统一了三个核心能力：
- 交互式工作台：数学家与 AI 代理通过一个活跃的证明蓝图进行协作，该蓝图将证明分解为可导航的步骤，供人类直接检查、指导和完善；
- 自动证明技能编排：结合自适应知识库搜索和 Lean 集成的迭代验证；
- 主题驱动的论文检索：将自动化形式化整合到经过验证的 Lean 知识库中。
利用 MathCoPilot，我们系统地比较了四个最先进的 LLM，包括 Gemini 3.1 Pro、GPT-5.4 和 Claude Opus 4.7，在 FormalMATH 子集以及两个需要深厚领域知识的实际 PDE 定理上，评估它们生成经过验证的 Lean 4 证明的能力，并识别故意错误证明中的错误。我们的结果显示，尽管当前模型在有利的自动形式化条件下能够高成功率地处理本科水平的问题，但在需要真正数学理解的领域特定定理上仍面临重大挑战。
博主点评： MathCoPilot 的提出标志着数学研究领域人机协作的新进展，尤其是在复杂定理的证明过程中。通过将人类的直觉与 AI 的计算能力相结合，该系统有望在未来推动数学研究的效率与深度。值得关注的是，尽管当前技术在处理基础问题方面表现良好，但对于更高级的数学挑战仍需进一步优化。