證明嵌入

深度分析

深度法則：利用 Lean4 證明嵌入量化選擇公理對自動定理證明的影響

本研究以Lean4追蹤選擇公理依賴，將Mathlib超過四十萬條定理分層，發現與深度相關的幾何異常分數可預測證明器成功率，顯示公理深度影響AI定理證明的實務表現。研究同時比較傳統符號求解器與神經導向混合策略，發現後者可將成功率提升至五倍，證實幾何指標在優化證明流程上的潛在價值。