Leanstral 1.5：人人皆可拥有的丰富证明
Mistral AI 发布了 Leanstral 1.5，这是一款旨在让形式化证明（formal proof）的生成变得更加普及和高效的新模型。该模型通过结合 Lean 定理证明器，能够自动生成数学证明，降低用户进入形式化验证领域的门槛，从而推动数学和软件验证的民主化。
背景速读
- **Mistral AI**是法国头部AI公司，主攻大语言模型。之前发布的几个模型对标GPT和Llama，但训练语料以英语为主、法语为辅，讲究推理效率。
- **Leanstral 1.5**是Mistral的新模型，专门面向“证明辅助”场景。所谓“证明辅助”指用计算机帮人写数学证明——比如用Lean、Coq这类工具——类似让AI充当数学家的“代码补全”。
- 这个模型的核心卖点是“稀缺变成富足”：传统上严格的形式化数学证明门槛极高、产出很少，Mistral认为通过专门训练的LLM可以把这条跑道变成任何人都能快速产出的领域。
- 背后的技术路线和Code Llama或StarCoder类似，即在一个通用底座上做数学/代码领域微调，但这次明确把“形式化验证语言”当成第一类公民处理。
- 为什么值得关注：形式化数学是AI安全、系统验证、高级推理的底层工具之一。如果LLM能可靠地生成经过机器验证的证明，会影响从芯片设计到加密协议的全链可靠度。这也是“AI辅助科学研究”的一个具体落点。