Gate News 消息，3 月 17 日，Mistral AI 今日發布 Leanstral，這是首個專為形式化驗證工具 Lean 4 設計的開源代碼 Agent。該模型的核心創新在於，AI 生成代碼的同時可輸出可被 Lean 4 自動校驗的形式化證明，從而繞開傳統 AI 代碼生成中人工審查的瓶頸環節。
Leanstral 採用稀疏 MoE 架構，擁有 120B 總參數和 6B 激活參數，以 Apache 2.0 協議開源，並針對 lean-lsp-mcp 進行了專項訓練優化。用戶可在 Mistral Vibe 中通過命令 /leanstall 零配置啟動，或通過免費 API 端點 labs-leanstral-2603 調用，同時支持下載權重進行自部署。
Mistral 同步發布了新評估基準 FLTEval，以 Lean 4 社區的費馬大定理形式化項目為測試場景。性能對比數據顯示：Leanstral pass@2 以 36 美元成本得分 26.3，超過成本 549 美元的 Claude Sonnet 4.6（23.7 分）；pass@16 以 290 美元成本得分 31.9，領先 Sonnet 8 分，而 Claude Opus 4.6 需 1,650 美元才能達到 39.6 分。在開源模型中，Qwen3.5-397B-A17B 需運行 4 次才能達到 25.4 分，仍低於 Leanstral pass@2 的表現。
