面向数学形式化证明：Mistral AI 发布 Leanstral 1.5 低使用成本开源模型

对于 PutnamBench 数学竞赛问题集中的题目，Leanstral 1.5 的平均解决开支仅有 4 美元，而 Seed-Prover 1.5 需要 300 美元以上，Aleph Prover 也需要 54~68 美元。