7月6日，欧洲人工智能企业MistralAI宣布推出Leanstral1.5模型，这是面向数学形式化证明程序语言Lean4的模型。该模型拥有119B参数，激活6B参数，并以Apache-2.0许可开源。在性能方面，Leanstral1.5在miniF2F形式数学基准测试的验证集和测试集上均实现了100%的完成率。在PutnamBench数学竞赛问题集中，Leanstral1.5能够解决672道Lean4问题中的587道，表现优异。

Leanstral1.5在成本效益方面同样表现出色，相较于其他模型，其解决PutnamBench数据集中问题的平均成本仅为4美元，远低于Seed-Prover1.5的300美元和AlephProver的54~68美元。在实际应用测试中，Leanstral1.5在57个代码库中标记了47个违规属性，其中11个指向了真实缺陷，包括5个此前未在GitHub上被报告过的问题，显示了其在实际场景中的有效性和准确性。