Leanstral – Mistral AI推出的首个开源AI代码智能体

Leanstral是什么

Leanstral 是Mistral AI推出的首个开源AI代码智能体，专为Lean 4定理证明器设计。模型采用120B总参数/6B激活参数的稀疏架构，能自动生成形式化证明并验证代码正确性。相比巨型竞品，Leanstral以极低成本（单次$18）实现更高效率，在真实数学代码库（如费马大定理项目）评测中表现优异。模型支持通过MCP协议扩展，已集成至Mistral Vibe平台。

Leanstral的主要功能

• 自动形式化证明生成：针对Lean 4证明助手，自动生成严格的数学证明和软件规范验证代码。