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 被設計為能夠處理需要數小時持續工作的長程任務。