Mistral發佈Leanstral：Lean4首個開源代碼Agent，生成代碼同時輸出形式化證明

據 1M AI News 監測，Mistral AI 今日發佈 Leanstral，首個專為形式化驗證工具 Lean 4 設計的開源代碼 Agent。AI 代碼生成的核心瓶頸是人工審查，Leanstral 讓 AI 生成代碼的同時輸出可被 Lean 4 自動校驗的形式化證明，繞開這一環節。模型採用稀疏 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。