深度分析
Formal Conjectures：以 Lean4 與 Mathlib 建構的研究級形式化猜想基準
面對自動推理系統快速進展，研究圈提出一套以Lean4形式化的Formal Conjectures基準。它以研究級開放猜想為核心，結合Mathlib與嚴格的Lean核心驗證流程，提供零污染的證明發現測試並同步支援已解題目的自動形式化。該庫已被用於推動新數學發現與建立可重複的評估標準。
Mathlib
速報
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驗證新證明，成功率四成。