LongCat-Flash-Prover：AI 攻克数学定理证明，不仅要“算得对”，更要“证得严”
LongCat-Flash-Prover是专为数学定理证明设计的大语言模型，旨在从“猜答案”转向“严谨证明”。它采用形式化语言Lean4，将证明过程拆解为自动形式化、草稿生成和证明生成三大原子能力。通过混合专家迭代框架，模型在冷启动和迭代阶段训练不同专家，并结合工具集成推理（TIR）来优化证明质量。在数据合成中，采用课程学习模式，从简单完整证明过渡到复杂引理式草稿证明，提高推理效率。模型还引入多个验证工具，如Lean4 Server、语义一致性检查和Theorem一致性，确保生成证明的语法正确性和语义一致性，防止作弊行为。实验结果表明，LongCat-Flash-Prover在MiniF2F-Test上以72次预算达到97.1%通过率，超越现有开源模型；在MathOlympiad-Bench等竞赛级任务上也取得显著进步。该模型已全面开源，不仅受到AI研究者关注，还引起了数学界的兴趣，有望成为数学研究和教育的基础设施，促进形式化数学的范式创新。