深度分析
OpenProver：結合 Lean4 與大型語言模型的代理式互動自動定理證明系統
隨著大型語言模型結合可驗證回饋，OpenProver以Planner-Worker-Verifier架構將Lean4形式驗證納入自動定理證明；系統支援互動式終端，讓使用者即時監控與引導證明流程。實驗顯示在ProofNet上的成功率比線性基線提升超過20%。
自動定理證明
深度分析
深度法則：利用 Lean4 證明嵌入量化選擇公理對自動定理證明的影響
本研究以Lean4追蹤選擇公理依賴，將Mathlib超過四十萬條定理分層，發現與深度相關的幾何異常分數可預測證明器成功率，顯示公理深度影響AI定理證明的實務表現。研究同時比較傳統符號求解器與神經導向混合策略，發現後者可將成功率提升至五倍，證實幾何指標在優化證明流程上的潛在價值。
深度分析
DreamProver：透過 wake–sleep 聚類與抽象化學習可重用引理，提升 LLM 證明成功率
自動定理證明領域近年受大型語言模型與形式化證明庫推動。DreamProver採用wake–sleep雙階段代理流程：醒期利用現有引理庫嘗試證題並產生候選中間引理，睡期對候選進行語義聚類、抽象與精簡並驗證後整合入庫。實驗顯示此法顯著提升解題率並減少證明長度與運算成本。