论文
MathCoPilot：数学研究人机共生范式的交互系统
MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research
摘要
既有基于LLM的定理证明器在形式数学基准上取得亮眼成绩，但仍局限于充当证明既定命题的自主智能体。本文提出MathCoPilot：一个体现数学研究新型人机共生范式的在环系统——数学家把握高层方向，AI智能体在持续人类指导下执行详细的形式化与证明工作。MathCoPilot统一三项核心能力：(1) 交互式工作台——数学家与AI智能体经活的证明蓝图协作，把证明分解为人类可直接检查、指示与精炼的可导航步骤；(2) 带自适应知识库搜索与Lean集成迭代验证的自动证明技能编排；(3) 主题驱动的论文检索与自动形式化进经验证的Lean知识库。使用MathCoPilot，我们系统比较四个最先进LLM（含Gemini 3.1 Pro、GPT-5.4与Claude Opus 4.7）：在FormalMATH子集与两个需要深厚领域专长的真实PDE定理上，评估其产出经验证的Lean 4证明及识别故意错误证明中错误的能力。结果显示：在有利的形式化条件下，当前模型能以高成功率处理本科级问题，但需要真正数学理解的领域专属定理仍存在实质挑战。
