Mistral AI 正式推出 Leanstral 1.5，一個專為 Lean 4 證明助手打造的開原始碼智慧體模型，引數規模達 119B，採用 Apache 2.0 許可，已在 Hugging Face 上架。該模型基於 Mistral Small 4 家族架構，每 token 僅啟用 6.5B 引數，兼顧效能與成本效率。
Leanstral 1.5 的核心定位是成為 Lean 4 環境中的 AI 程式設計與證明夥伴。Lean 4 本身是一種強大的證明助手，能夠表達極其複雜的數學結構——例如 完美空間（perfectoid spaces）——以及形式化軟體規範，如 Rust 程式碼片段的屬性驗證。這意味著 Leanstral 1.5 的應用場景遠不止通用程式碼生成，而是直接切入數學定理證明、形式化驗證等高門檻、高價值的科研與工業領域。
在技術架構上，該模型採用了 混合專家（MoE） 設計，共包含 128 個專家，每個 token 啟用其中 4 個。這種稀疏啟用機制使得模型在保持 119B 總引數規模的同時，推理計算量僅相當於一個約 6.5B 啟用引數的稠密模型。模型支援 文本與影像多模態輸入，上下文視窗達 256k token，官方建議在實際使用中控制在 20 萬 token 以內以保證穩定性。
部署方面，Mistral 提供了兩條路徑。使用者可以直接通過 Mistral API 呼叫，無需訂閱 Pro 計劃，只需在賬戶設定中開啟“Labs models”選項並生成 API 金鑰，再通過 Mistral Vibe CLI 工具即可啟動 Leanstral 智慧體。對於偏好本地部署的使用者，模型同樣相容 vLLM 推理框架，官方給出了詳細的伺服器啟動引數與客戶端呼叫示例，推薦使用張量並行（tensor parallelism）為 4 的配置，並啟用 Flash Attention MLA 後端以最佳化長上下文推理效率。
Leanstral 1.5 的釋出延續了 Mistral 在開源模型領域的激進策略。與閉源的通用大模型不同，Leanstral 1.5 聚焦於一個極為細分的專業賽道——形式化數學與軟體驗證。這一領域長期以來由人類專家主導，自動化程度有限。AI 程式碼智慧體的介入，有望大幅降低 Lean 4 的使用門檻，加速數學研究中的證明編寫與檢查流程，同時為安全關鍵軟體（如作業系統核心、加密協議）提供更高效的形式化驗證手段。
從產業視角看，Leanstral 1.5 的出現可能對算力需求結構產生微妙影響。數學證明與形式化驗證任務通常需要長時間的鏈式推理，對模型的長上下文處理能力和推理連貫性要求極高，這與通用對話或程式碼補全的負載特徵不同。若此類專用模型在學術界和工業界獲得採用，可能會催生對高吞吐、長上下文推理最佳化的算力需求，間接影響 AI 基礎設施層 的硬體與軟體棧設計。
此外，Leanstral 1.5 基於 Mistral Small 4 家族構建，表明 Mistral 正在將其基礎模型能力向多個垂直方向延伸。此前 Mistral 已在通用對話、程式碼生成等領域佈局，此次切入數學證明，進一步豐富了其開源模型矩陣。在開源社群中，一個專攻 Lean 4 的強模型可能吸引更多研究者參與形式化數學與驗證工具的生態建設，形成正向迴圈。
Mistral 同時提醒，該模型是對此前 Leanstral 版本的更新迭代，建議使用者通過 lean-lsp-mcp 工具與 Leanstral 互動，以獲得更流暢的開發體驗。對於複雜任務，官方推薦將推理強度（reasoning effort）設為“high”，並允許模型進行長時間、多步驟的問題求解——Leanstral 被設計為能夠處理需要數小時持續工作的長程任務。