Mistral推出開源模型Leanstral，專為Lean 4形式化證明工作流程設計

法國AI公司Mistral AI發布開源模型Leanstral，針對Lean 4工作流程，並以程式碼代理形式提供，除了生成程式碼之外，Leanstral也能處理形式化證明相關工作。官方同時以Apache 2.0授權釋出模型權重，整合至Mistral Vibe代理模式，並提供labs-leanstral-2603實驗性API端點，讓開發者可透過雲端或自建環境使用。

Leanstral鎖定Lean 4工作流程，而非一般用途的程式開發助理。Lean 4是一套用於形式化證明的證明助理與程式語言，可用來表達數學定理與軟體規格，Mistral表示，Leanstral的訓練目標是讓模型能在較貼近實務的形式化儲存庫中作業，而不是只解單一數學題或只包裝大型通用模型，官方也強調，該模型支援MCP，並特別針對常用的lean-lsp-mcp進行能力調校。

Mistral將Leanstral直接納入Mistral Vibe。依官方模型頁說明，使用者可在Vibe內透過/leanstall指令安裝Leanstral代理，也可改以vLLM在本地端部署模型。Hugging Face模型頁也顯示，Leanstral採稀疏MoE架構，支援工具呼叫、長上下文與多語能力。

Mistral此次也同步提出名為FLTEval的新基準測試，作為Leanstral的主要評測依據。官方說明，FLTEval不是用競賽數學題評估，而是以FLT專案拉取請求中的形式化證明補完與新概念定義為測試情境。Mistral公布的數字顯示，Leanstral在pass@2時得分26.3，高於官方列出的Claude Sonnet 4.6的23.7，而在pass@16時得分31.9，但Claude Opus 4.6仍以39.6領先。

官方在案例中舉出兩類應用。一類是處理新版本Lean造成的相容性問題，例如協助找出def與abbrev在定義等價上的差異，修正rw tactic無法匹配的情況，另一類則是把Rocq中的語義定義轉寫為Lean，並進一步完成部分程式性質證明。就目前公開資訊來看，Mistral這次發布的產品變動，主要是把開源程式碼代理的範圍，從一般軟體實作再往形式化驗證場景延伸。

Mistral也預告後續將釋出技術報告，進一步說明Leanstral的訓練方法，並公開FLTEval，以補足現有評測偏重競賽數學題的限制。現階段Leanstral已可從Hugging Face模型頁與Mistral Vibe相關說明頁取得與部署。