深度分析
OpenProver：結合 Lean4 與大型語言模型的代理式互動自動定理證明系統
隨著大型語言模型結合可驗證回饋，OpenProver以Planner-Worker-Verifier架構將Lean4形式驗證納入自動定理證明；系統支援互動式終端，讓使用者即時監控與引導證明流程。實驗顯示在ProofNet上的成功率比線性基線提升超過20%。
Lean4
深度分析
深度法則：利用 Lean4 證明嵌入量化選擇公理對自動定理證明的影響
本研究以Lean4追蹤選擇公理依賴，將Mathlib超過四十萬條定理分層，發現與深度相關的幾何異常分數可預測證明器成功率，顯示公理深度影響AI定理證明的實務表現。研究同時比較傳統符號求解器與神經導向混合策略，發現後者可將成功率提升至五倍，證實幾何指標在優化證明流程上的潛在價值。
深度分析
Lean4Agent：以 Lean4 依賴類型語言建構 LLM 代理工作流程的形式驗證框架
隨著大型語言模型在高風險領域的應用增多，Lean4Agent 以依賴類型的 Lean4 語言提供工作流程與執行軌跡的形式化建模與驗證，實驗顯示驗證通過的流程在軟體工程基準上提升約12%，並透過 LeanEvolve 進一步提升7%的效能。此技術有望推動 AI 代理的安全與自我優化。
深度分析
Formal Conjectures：以 Lean4 與 Mathlib 建構的研究級形式化猜想基準
面對自動推理系統快速進展，研究圈提出一套以Lean4形式化的Formal Conjectures基準。它以研究級開放猜想為核心，結合Mathlib與嚴格的Lean核心驗證流程，提供零污染的證明發現測試並同步支援已解題目的自動形式化。該庫已被用於推動新數學發現與建立可重複的評估標準。
深度分析
OpenCLAW-P2P v6.0：多層持久化與Lean4形式化驗證下的去中心化AI同行評審
OpenCLAW-P2P v6.0 將去中心化自律 AI 評審平台推向生產級運作，核心在於四層文件持久化（記憶快取、Gun.js、Cloudflare R2、GitHub 備份）、多模型細緻評分、Lean4 形式化驗證與即時參考查證代理。
深度分析
Lean Atlas 與 Lean Compass：以 Lean4 自動剪枝縮減語意審核範圍
面對AI自動形式化的語意幻覺問題，本研究以Lean Atlas與Lean Compass將Lean4專案按型別分級並篩除不可影響語意的證明依賴，將人工審核候選大幅縮小，並提出aligned Lean code作為人機協作的品質標準，工具可跨數學、物理與密碼學領域使用。
深度分析
Project Yanasse：以 DeepVision 類比將 Mathlib 中 Lean4 戰術從機率論移植至表示論並生成新證明
研究以DeepVision類比把一領域的Lean4戰術模式轉移到遙遠領域。方法統計戰術分佈、以NP難度配對比對證明狀態，並由AI語義轉寫戰術。Probability→RepresentationTheory十次嘗試產生四個Lean驗證新證明，成功率四成。