近日，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%，两项成绩均刷新了该类模型的纪录。 成本优势是本次发布中的另一显著亮点。Mistral AI 特别强调，Leanstral1.5 大幅降低了科研试错的资金门槛。举例来说，在 PutnamBench 中求解一道题，使用 Leanstral1.5 平均仅需 4 美元；而对比模型 Seed-Prover1.5 的开销超过 300 美元，Aleph Prover 也在 54 至 68 美元之间。这种量级的成本压缩，意味着高精度数学证明辅助技术不再是少数实验室的专属工具。 在实际代码开发场景中，Leanstral1.5 的“找茬”能力同样值得关注。针对 57 个代码库的实测，它成功识别出 47 个违规属性，其中 11 个经核实为真实缺陷。更值得关注的是，这 11 个缺陷里有 5 个此前从未在 GitHub 上被报告过。这表明 AI 在程序验证与安全审查方面，已不仅是“锦上添花”，而是能够切实发现未知隐患。 随着 Leanstral1.5 的开源，数学界与计算机科学界正迎来一个更低门槛、更高效的证明辅助工具。算力成本降低，经济压力减小，数学形式化证明的普及速度自然随之提升。科研人员终于能从繁琐的计算与核对中解放出来，将更多精力投入到核心科学问题的突破上。