定理證明也開始捲成本：Mistral開源Leanstral 1.5，每題約4美元

Mistral AI 開源 Leanstral 1.5，一款面向 Lean 4 形式化證明的模型。模型總引數量 1190 億，啟用引數約 65 億，採用 Apache-2.0 協議，並提供免費 API 訪問。 官方評測顯示，Leanstral 1.5 在 PutnamBench 672 道題中解出 587 道；在抽象代數基準 FATE-H 和 FATE-X 上分別達到 87% 和 34%，重新整理同類模型最佳表現。 Leanstral 1.5 在 PutnamBench 上的平均解題成本約為 4 美元，低於此前部分系統數十至數百美元的成本。隨著單題 token 預算提高，它的解題數量持續增加；在 AVL 樹複雜度證明中，模型經過超過 270 萬 token 推理和 22 次上下文壓縮，最終完成相關證明。 除數學證明外，Leanstral 1.5 還被用於程式碼驗證。團隊在 57 個開源 Rust 倉庫中發現 11 個真實 bug，其中 5 個此前未被報告。 [動察 Beating]