摘要
现有基于大语言模型的定理证明器多作为自主代理运行，局限性明显。本文提出 MathCoPilot，一种体现人机共生新范式的人机协同系统：数学家把控高层数学方向，AI 代理在持续人类指导下执行详细的形式化与证明工作。该系统统一了三大核心能力：支持通过动态证明蓝图协作的交互式工作台、具备自适应知识库搜索与 Lean 集成迭代验证的自动化证明技能编排，以及主题驱动的论文检索与自动形式化机制。实验表明，当前模型在处理本科级问题时表现良好，但在需深层领域理解的定理上仍面临挑战。
AI 推荐理由
论文聚焦数学定理证明与形式化推理，核心在于提升 LLM 的深层逻辑推理能力。
研究机构
State Key Laboratory of Cognitive Intelligence, University of Science and Technology of China
School of Mathematical Sciences, University of Science and Technology of China
论文信息