为什么重要
FLTEval 代表了 AI 形式化推理评测的新方向。与传统的竞赛数学证明不同，它要求模型在真实的费马大定理（Fermat’s Last Theorem）Lean 4 形式化项目中工作——完成 PR 级别的证明补全和数学概念定义。由 Mistral AI 随 Leanstral 模型一同发布，是首个面向生产级形式化证明工程的 benchmark。
核心设计
- 仓库级：模型需理解整个 FLT 项目的上下文，而非孤立的题目
- PR 风格：任务模拟真实的 Pull Request 工作流，包括证明补全和新概念定义
- Lean 编译器验证：不依赖 LLM 评判，由 Lean 4 编译器直接判定正确性，零歧义
关键发现
- 极高难度：最强模型仅 39.6% 通过率，证明形式化推理仍是 AI 的重大挑战
- Anthropic 领先：Claude Opus 4.6 以 39.6% 大幅领先，比专门训练的 Leanstral 高出近 18 个百分点
- 中间集群密集：第 2-4 名仅相差 1.8 个百分点（21.9%-23.7%），区分度有限
- 目前仅 4 个模型被评测，生态尚在早期
关联基准
- FrontierMath：研究级数学推理
- OmniMath：开放式数学问题
- MATH：竞赛数学题集