背景：

    近年来，结合大语言模型和形式化语言的自动定理证明领域越来越受到关注。2024年Google deepmind推出形式化证明系统Alphaproof，在2024年IMO中取得银牌水平。2025年，美国AI4MATH创业公司Harmonic的形式化系统Aristotle以及字节跳动的Seed Prover在2025年IMO中达到金牌水平。随着高中竞赛被攻克，人们将目光投向了更高层次的大学数学以及前沿数学。

成果：

    中国科学院数学院数学机械化实验室 刘俊杞研究生，支丽红研究员，数学所何伟鲲副研究员与开源AI4MATH组织Numina及其他高校合作提出一种全新的形式化定理证明Agent——Numina-Lean-Agent，在形式化定理证明和自动形式化方面达到了世界最先进的性能。Numina-Lean-Agent 成功形式化证明了 2025 年 William Lowell Putnam 数学竞赛（世界上最难的大学数学竞赛）的全部 12 道试题，达到了当前世界最先进的性能水平。该结果与AxiomMath的闭源系统 AxiomProver的表现持平，并优于 Harmonic 的 Aristotle以及字节跳动的Seed-Prover 1.5。

除了一般的形式化自动定理证明任务之外，Numina-Lean-Agent 还可作为一个通用的数学推理系统，支持数学家进行交互式的“vibe proving”。利用该系统与人类专家协作，在两周时间内完成了对数学所何伟鲲副研究员的论文Effective Brascamp-Lieb inequalities形式化，展示了强大的人机交互能力。

Publication:

https://arxiv.org/abs/2601.14027

Code: https://github.com/project-numina/numina-lean-agent