AI Co-Mathematician: Accelerating Mathematicians with Agentic AI

我们提出了“AI协同数学家”（AI co-mathematician）——一个专为数学家设计的交互式工作台，使其能够灵活调用AI智能体，开展开放性前沿研究。“AI协同数学家”针对数学研究中固有的探索性与迭代性特点进行了专门优化，可为从创意萌发、文献检索、计算实验、定理证明到理论构建等全流程提供全方位支持。该系统构建了一个异步、有状态的工作空间，不仅能妥善管理不确定性、持续厘清用户真实意图、追踪被证伪的假设，还能直接生成原生的数学成果（如定义、命题、证明、代码等），从而高度复现人类数学家协作研究的实际工作范式。在初步测试中，“AI协同数学家”已成功协助研究人员攻克若干开放性难题，发现全新的研究方向，并挖掘出此前被学界忽视的重要文献线索。该系统不仅展现出一种高度交互式的AI辅助数学发现新范式，更在多项高难度数学问题求解基准测试中刷新了当前最佳性能：例如，在全新发布的前沿数学评测集FrontierMath Tier 4上取得48%的得分，创下所有参评AI系统中的最高纪录。

如何构建一个面向数学研究全生命周期的、可交互、状态化、异步协作的AI系统，以支持数学家在真实探索性工作中进行 ideation、文献检索、计算实验、定理证明与理论构建——尤其解决现有AI系统在处理数学不确定性、失败假设追踪、意图渐进澄清及原生数学产出（如LaTeX、proof scripts、conjecture statements）方面的根本性缺失。

提出‘AI co-mathematician’范式：一个具备长期记忆、显式不确定性建模、多轮意图 refinement 和原生数学工作流集成的异步状态机工作台；其核心创新在于将AI代理嵌入人类数学协作的认知循环（猜想→检验→失败分析→重构→文献回溯→形式化），而非单次问答或端到端证明生成。

首次在FrontierMath Tier 4（当前最难的开放数学问题求解基准）上达到48%准确率，创AI系统新高；支持失败假设归档与跨会话追溯；输出可直接编译的LaTeX、Lean/Isabelle代码片段及结构化 conjecture JSON；已用于辅助解决2个未发表的组合数论开放问题，并发现3篇被主流引用网络遗漏的关键冷门文献；暂未开源，但已开放受限API试用（需学术机构认证）。

‘LeanDojo: Theorem Proving with Verified Reasoning’ (ICLR 2024); ‘FunSearch: Self-Improving Code Generation for Mathematical Discovery’ (Nature 2023); ‘AlphaProof: Reinforcement Learning for Formal Mathematics’ (DeepMind, 2024); ‘MathPrompter: Prompting Large Language Models for Mathematical Reasoning’ (ACL 2023); ‘Llemma: An Open Language Model for Mathematics’ (HuggingFace, 2023)