摘要： Mistral 開源首個專為 Lean 4 證明工程打造的程式代理 Leanstral，總參數 120B、每次推論啟用約 6B。它以 Apache 2.0 完整開放，能部署在團隊自己的硬體上，供形式驗證流程使用。文中也提醒與 Qwen 系列的比較需等獨立評測，不能只依賴發布討論。
Leanstral 登場：開源陣營首個專為 Lean 4 而生的程式代理，出自 Mistral 之手。這款模型名為 Leanstral-120B-A6B，採稀疏架構，總參數 120B、每次推論實際啟用約 6B，權重依 Apache 2.0 完整開放；Hugging Face 上的模型卡（mistralai/Leanstral-2603）登錄的規格則是 119B-A6B。Mistral 沒把它當展示品包裝，而是讓它承擔真正的證明工程——走進完整的儲存庫補齊證明、把概念定義出來，而非解決彼此孤立的練習題。對從事形式驗證的團隊來說，同級工具中首度出現能裝在自己機器上執行的選擇。
Lean 4 領域首個開源專用代理
一般程式代理交出的是「看似正確」的程式碼；Lean 4 的世界卻只存在兩種狀態：通過機器驗證，或是不成立。Mistral 的切入角度，是讓代理正面迎向這個高門檻領域——訓練以 lean-lsp-mcp 為對象，並支援任何 MCP 伺服器，代理因此能真的對 Lean 專案狀態進行讀取與寫入。Hacker News 上的討論呈現了典型反應：方向獲得普遍認同，但與 Qwen 系列孰優孰劣，社群選擇保留判斷，待獨立評測出來再下定論。
為何挑上 Lean 4
Lean 4 是一套證明助理，既表達得了 perfectoid space 這類位處前沿的數學物件，也寫得出軟體規格——Rust 程式碼的已驗證性質便是例子。它的關鍵價值，在於把「人類審查機器產生的程式碼」這道瓶頸，替換成「機器自己證明」：證明一旦通過，正確性就成了數學事實。隨著 AI 生成程式碼的數量爆量，形式驗證正從數學系的奢侈品，轉變為高風險軟體的必需品——Leanstral 押注的便是這股走向。
120B 總量、6B 啟用背後的成本帳
稀疏架構在這裡不是省錢的口號，而是整個產品成立的邏輯。證明搜尋本質上是規模龐大的平行嘗試，單次推論必須夠便宜，pass@k 這類多次取樣的策略才有意義：跑一次 18 美元，十六次合計也不過 290 美元。相較之下，Claude Opus 一趟要價 1,650 美元，是 Leanstral 單次成本的 92 倍。Mistral 的盤算很直接：以一個便宜、能平行疊代的專用模型，去換在垂直領域與通用旗艦模型長期周旋的籌碼。
FLTEval 數字怎麼看
FLTEval 以 FLT 專案的真實 PR 作為題庫，成績如下：Claude Haiku 花費 184 美元換到 23.0 分，Sonnet 花費 549 美元拿下 23.7 分，Opus 花費 1,650 美元得到 39.6 分。Leanstral 跑單次（18 美元）得 21.9；pass@2（36 美元）升到 26.3，以大約 15 分之一的成本越過 Sonnet；pass@16（290 美元）推到 31.9，領先 Sonnet 8 分。開源陣營的其他選手上，Qwen3.5-397B-A17B 要取樣 4 次才達 25.4，Kimi-K2.5-1T-A32B 約在 20.1，GLM5-744B-A40B 約在 16.6——專用化在這份基準上確實收到了成效。天花板依舊是 Opus 的 39.6，但換算成每一分的成本，雙方完全是不同的量級。
三種入手與執行管道
入手有三條途徑。第一，零設定的 Mistral Vibe：下達 /leanstall 指令、以 Shift+Tab 選定 Leanstral，或直接用 vibe —agent lean 開啟。第二，API：端點名稱 labs-leanstral-2603，在限定期間內免費、或只收極少費用。第三，自行架設：取得 Apache 2.0 權重，部署在自己的硬體上。對受監管環境、或不願讓程式碼離開自己環境的團隊而言，第三條途徑才是關鍵——這也正是開源權重到了 2026 年依然稀缺的價值。