深度分析
Axle 雲端平台提供 14 項 Lean 4 元程式工具，提升 AI 證明效能
隨著AI在數學領域的快速發展，對Lean4工具的高併發與嚴格驗證需求日增。Axle提供十四項元程式工具，支援多版本、每請求隔離，並可在雲端以每秒超過兩次的效能驗證證明。此服務已支援超過五億次請求，成為2025年Putnam競賽滿分背後的基礎設施。
Mathlib
深度分析
Formal Conjectures：以 Lean4 與 Mathlib 建構的研究級形式化猜想基準
面對自動推理系統快速進展，研究圈提出一套以Lean4形式化的Formal Conjectures基準。它以研究級開放猜想為核心，結合Mathlib與嚴格的Lean核心驗證流程，提供零污染的證明發現測試並同步支援已解題目的自動形式化。該庫已被用於推動新數學發現與建立可重複的評估標準。
速報
MathlibPR：以 LLM 評估 Lean/Mathlib Pull Request 的基準初探
背景：Lean與Mathlib為LLM輔助形式化推理的主流。方法：提出MathlibPR基準，從Mathlib4真實PR歷史擷取資料並設計分階段評估，測試多款大型語言模型與代理人。結果：模型難以區分可合併PR與僅通過建置但未合併的PR，MathlibPR提供審查輔助的監督信號。
深度分析
Project Yanasse：以 DeepVision 類比將 Mathlib 中 Lean4 戰術從機率論移植至表示論並生成新證明
研究以DeepVision類比把一領域的Lean4戰術模式轉移到遙遠領域。方法統計戰術分佈、以NP難度配對比對證明狀態，並由AI語義轉寫戰術。Probability→RepresentationTheory十次嘗試產生四個Lean驗證新證明，成功率四成。