近日，mistral ai 正式推出面向数学形式化证明语言 lean4 的开源大模型 —— leanstral1.5。该模型遵循 apache-2.0 开源许可协议，拥有总计 119b 的参数量，其中激活参数为 6b，在保障强大推理能力的同时显著压缩了部署与运行开销。
作为一款深度聚焦数学逻辑推理的专用智能体，Leanstral1.5 在多项权威评测中交出了令人瞩目的答卷。在 miniF2F 这一经典形式化数学基准测试中，模型在验证集与测试集上均实现了 100% 的命题完成率。在难度极高的 PutnamBench 数学竞赛题库（含 672 道 Lean4 编码题目）中，成功求解 587 道；而在抽象代数专项评估 FATE 系列中，其表现同样突出：在硕士级难度的 FATE-H 测试中达成率达 87%，在博士级挑战 FATE-X 中亦取得 34% 的通过率，刷新同类模型历史最佳成绩。
☞☞☞AI 智能聊天, 问答助手, AI 智能搜索, 多模态理解力帮你轻松跨越从0到1的创作门槛☜☜☜
成本效益成为本次发布的另一关键突破。Mistral AI 指出，Leanstral1.5 显著降低了数学形式化研究的试错门槛。以 PutnamBench 题目为例，单题平均求解成本仅为 4 美元；相较之下，Seed-Prover1.5 的单题开销超过 300 美元，Aleph Prover 则介于 54 至 68 美元之间。如此大幅的成本削减，有望推动高精度证明辅助技术从高端实验室走向更广泛的学术与工程实践场景。
在真实代码审查任务中，Leanstral1.5 同样展现出卓越的缺陷识别能力。针对 57 个开源 Lean 项目进行实测，模型共发现 47 处潜在违规行为，其中 11 项经人工确认确为真实漏洞。尤为值得关注的是，有 5 个漏洞此前从未在 GitHub 上被公开报告或追踪，充分印证了 AI 在程序验证与安全审计领域的前沿价值。
随着 Leanstral1.5 的全面开源，数学与计算机科学交叉领域正迎来一个更轻量、更经济、更易用的形式化证明新范式。通过降低算力依赖与使用成本，该模型有望加速数学定理的机器可验证进程，助力研究者摆脱重复性验证负担，将精力集中于更具创造性的理论探索与科学突破。
