Mistral AI 发布 Leanstral 形式化证明专用模型

Mistral AI 于2026年3月16日发布面向Lean 4形式化证明工程的专用代码模型Leanstral，主题为Leanstral-120B-A6B。模型针对真实形式化仓库操作训练，总参数120B、激活参数6B。发布同步开放模型权重（Apache 2.0许可）、免费API端点及Vibe中的代理使用方式。输入为文本与代码，输出为文本、代码及形式化证明，上下文长度未知。