美团龙猫团队开源 LongCat-Flash-Prover：让AI真正“懂”数学证明

2026年3月24日，美团旗下研究团队“龙猫”正式开源了一款专为数学形式化证明设计的AI模型——LongCat-Flash-Prover。这不是又一个能“猜答案”的大模型，而是一个能像数学家一样，一步步写出完整、可验证证明的系统。

过去，AI在数学题上常靠“猜”——看到题干，根据训练数据模仿出一个看起来合理的答案。但真正的数学证明，容不得半点模糊。LongCat-Flash-Prover 的核心突破在于，它把证明过程拆解成三个清晰、可控制的步骤：

• 自动形式化（Auto-Formalization）：把人类写的数学问题，精准翻译成Lean4语言——一种被数学界广泛接受、计算机可验证的形式语言。
• 草稿生成（Sketching）：像人类写证明前先列提纲一样，模型先规划出关键引理、结构框架，而不是直接硬算。
• 证明生成（Proving）：在框架内逐条填充逻辑，每一步都经过形式化校验，确保无漏洞。

不是靠算力堆出来的，是靠设计赢的

在权威基准测试MiniF2F-Test中，LongCat-Flash-Prover 只用了72次推理尝试，就达到了97.1%的通过率——这个数字，比此前所有开源模型都高，且用的计算资源更少。不是靠“暴力试错”，而是靠更聪明的推理路径。

在更高难度的竞赛题库中，它也表现突出：

• MathOlympiad-Bench：在IMO级别题目中，正确率领先第二名近15个百分点。
• PutnamBench：美国大学生数学竞赛（Putnam）的真题，模型能独立完成超过80%的证明，其中近半数被人类评审确认为“清晰、严谨”。

不是黑箱，是能被“检查”的证明机器

很多人担心AI做证明是“黑箱操作”。LongCat-Flash-Prover 的设计从一开始就杜绝了这一点。

模型内置了完整的校验链：

• 每一次生成的Lean代码，都会自动提交给Lean4Server实时验证——不通过，就重来。
• 系统会检测是否存在“偷懒”行为：比如直接复制训练数据中的证明、用错误的定理替换、或绕过前提条件。
• 针对9种已知的“作弊”模式（如诱导模型调用不存在的引理），模型都做了针对性防御。

训练阶段，团队还引入了“分层掩码”和“Token老化控制”技术——简单说，就是让模型在学证明时，不能只盯着最后一步，必须理解每一步之间的依赖关系。这使得模型在使用混合专家架构（MoE）时更稳定，不容易“跑偏”。

它不只是一个工具，是数学研究的新助手

我们见过太多AI在数学题上“炫技”，但很少有模型真正被数学家用起来。LongCat-Flash-Prover 的目标不同：它不是要取代数学家，而是成为他们的“协作者”。

已经有数学研究者开始尝试用它：

• 一位剑桥博士生用它辅助完成了关于拓扑群的两个引理的正式化，原本需要两周的工作，模型在两天内给出了可验证草稿。
• ArXiv上已有论文在附录中注明：“部分证明由LongCat-Flash-Prover生成并经人工验证”。

它不追求“刷榜第一”，而是追求“能用、可信、可复现”。这正是学术界最需要的AI工具。

现在就能用

模型、代码、完整技术报告均已开源，任何人都可以下载、运行、验证。

GitHub 仓库：
https://github.com/meituan-longcat/LongCat-Flash-Prover

Hugging Face 模型：
https://huggingface.co/meituan-longcat/LongCat-Flash-Prover

完整技术报告（PDF）：
https://github.com/meituan-longcat/LongCat-Flash-Prover/blob/main/LongCat_Flash_Prover_Technical_Report.pdf

如果你是数学研究者、形式化验证工程师、或只是对“AI如何真正理解数学”感兴趣，这个项目值得你花时间试一试——它不是噱头，是实打实的进展。