AI 代理在程式碼生成方面已展現出高度能力。然而，當我們將這些模型推向從前沿數學研究到任務關鍵軟體的各種高風險領域時，會遇到一個規模瓶頸：人工審查。手動驗證所需的時間和專業知識成為工程速度的主要阻礙。

我們設想一種更有幫助的程式碼代理，能夠同時執行任務並根據嚴格的規格正式驗證其實現。人類不再需要除錯機器生成的邏輯，而是可以指示他們想要什麼。今天，我們正朝著這個願景邁出第一大步。

我們發布了 Leanstral，這是第一款專為 Lean 4 設計的開源程式碼代理。Lean4 是一個證明輔助工具，能夠表達複雜的數學對象，如完美空間，以及軟體規格，如 Rust 片段的屬性。與現有的、作為大型通用模型包裝器或專注於單一數學問題的證明系統不同，Leanstral 的設計目標是極其高效（擁有 6B 活躍參數），並針對在真實的正式儲存庫中運作進行了訓練。

開放且易於存取：我們根據 Apache 2.0 授權發布了 Leanstral 的權重，並在 Mistral vibe 中提供代理模式，以及透過免費的 API 端點存取。我們還將發布一份技術報告，詳細說明我們的訓練方法，以及一個新的評估套件 FLTEval，以將評估從對競賽數學的關注轉移。

高效且強大：我們為 Leanstral 使用了高度稀疏的架構，並針對證明工程任務進行了優化。透過利用 Lean 作為完美驗證器的平行推理，Leanstral 相較於現有的閉源競爭對手，不僅效能高，而且成本效益高。

可透過 MCP 升級：Leanstral 透過 vibe 支援任意 MCP，並經過專門訓練，以在常用的 lean-lsp-mcp 上達到最大效能。

為了反映在真實證明工程場景中的實用性，我們對 Leanstral 進行了基準測試，以完成 FLT 專案中每個 PR 的所有形式證明和正確定義新的數學概念，而不是孤立的數學問題。我們將 Leanstral 與領先的程式碼代理（Claude Opus 4.6、Sonnet 4.6、Haiku 4.5）和開源模型（Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40B）進行了比較。

Leanstral-120B-A6B 相較於其體積大得多的開源同類產品，展現了顯著的效率優勢。雖然 GLM5-744B-A40B 和 Kimi-K2.5-1T-32B 等模型在擴展方面遇到困難，其 FLTEval 分數分別約為 16.6 和 20.1，但 Leanstral 僅需一次通過即可超越它們。

即使是 Qwen3.5-397B-A17B，最強的 OSS 競爭對手，也需要 4 次通過才能達到 25.4 的分數。相比之下，Leanstral 在一半的投入（pass@2）下就達到了更高的 26.3 分，並持續線性擴展，在相同的成本水平下達到 29.3 分。

Leanstral 為 Claude 套件提供了一個高價值的替代方案，以極低的價格提供競爭力的效能：Leanstral pass@2 達到 26.3 分，比 Sonnet 高 2.6 分，而運行成本僅為 36 美元，而 Sonnet 則為 549 美元。在 pass@16 時，Leanstral 達到 31.9 分，比 Sonnet 高 8 分。雖然 Claude Opus 4.6 仍然是品質領導者，但其成本高達 1,650 美元，是運行 Leanstral 的 92 倍。

在我們的基準測試中，我們使用了 Mistral Vibe 作為框架，沒有對評估進行任何修改。

當新的 Lean 版本出現重大變更時，遷移程式碼可能是一場巨大的噩夢。我們將一個來自 Proof Assistants Stack Exchange 的真實問題餵給 Leanstral，該問題關於一個在 Lean 4.29.0-rc6（由於其新穎性，我們未對其進行訓練）中神秘停止編譯的腳本。罪魁禍首是一個重寫（rw）策略，它突然無法匹配涉及簡單類型別名的模式，最初寫為 def T2 := List Bool。

Leanstral 並沒有漫無目的地猜測，而是捲起袖子開始工作。它成功地構建了測試程式碼來重現失敗的環境，並診斷了定義相等性方面的根本問題。該模型正確地識別出，由於 def 創建了一個需要顯式展開的嚴格定義，它正在積極阻止 rw 策略看到它需要匹配的底層結構。

它提出的修復很簡單：只需將 def 替換為 abbrev。因為 abbrev 創建了一個透明的別名，它立即在定義上等於原始類型，所以 rw 策略可以再次完美地匹配證明中的模式（L2 n）.length。Leanstral 完成了工作，並向使用者完美地解釋了其原理。

我們將 Rocq 中的定義從 https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html 複製過來，並要求 Leanstral 轉換為 Lean。它成功地做到了，甚至實現了自訂符號。範例片段：

它還可以將 Rocq 語句（沒有證明）翻譯成 Lean，然後證明該語言中程式的一些屬性：

Leanstral 今日對所有人開放使用。

Mistral Vibe 中的零設定：我們已將 Leanstral 直接整合到 Mistral Vibe 中，實現即時、零設定的 vibe 編碼和證明。使用 /leanstall 進行啟用。然後要使用 Leanstral，請按 Shift+Tab 直到模型顯示為 Leanstral。或者，使用 vibe --agent lean。

Labs API：透過我們免費/近乎免費的 API 端點 labs-leanstral-2603 存取模型。我們將在有限的時間內保持此端點的高度可及性，以收集真實的意見回饋和可觀察性數據，為下一代驗證程式碼模型提供動力。

擁有權重：下載 Apache 2.0 授權的模型，並在您自己的硬體上運行它。