LongCat-Flash-Prover：AI 攻克数学定理证明，不仅要“算得对”，更要“证得严”
美团开源了数学定理证明专用模型，推动 AI 从猜答案到形式化严谨推理。
数学定理证明要求极端严谨的逻辑链条，自然语言含糊一点就全盘崩塌。美团开源了专用模型 LongCat-Flash-Prover，让 AI 从“猜答案”转向“形式化证明”，用机器可验证的语言写出滴水不漏的推理步骤。这是复杂推理能力的一次关键跃升。
正文摘录
 LongCat-Flash-Prover：AI 攻克数学定理证明，不仅要“算得对”，更要“证得严” 美团技术团队 2026-04-07 LongCat 大模型 开源 引言 现如今的大语言模型已经能流畅地写文章、写代码，甚至执行复杂的 Agent 工作流，然而，它们在面对严谨的数学定理证明时，却往往显得力不从心。 在常规的数学解题中，模型只需要“答对最终数值”即可，但数学定理证明不同，它要求极度严苛的逻辑链条，任何一句自然语言的模棱两可，都可能导致整个证明的崩塌。那么，如何让 AI 从“猜答案”走向“严谨证明”，成为复杂推理具有挑战的课题。 为了解答这个问题，我们开源了专门用于数学形式化与定理证明的模型 —— LongCat-Flash-Prover 。  LongCat-Flash-Prover 在解决定理证明和形式化任务时，将形式化推理拆解为自动形式化（Auto-Formalization）、草稿生成（Sketching）和证明生成（Proving）三大原子能力。在结合工具集成推理（Tool-Integrated Reasoning，TIR）策略下， 仅用 72 次推理预算，MiniF2F-Test 通过率就达到 97.1% ，在已知开源 Prover 模型中刷新 SOTA；