Advances in Deep Learning for Mathematical Theorem Proving
summary
Google project augments a brute‑force ATP called improver with deep learning to rank axioms and guide proof search, using the Mizar (58k statements) corpus. A dual‑branch encoder scores candidate lemmas for premise selection and a similar model ranks clauses during search; definition embeddings + 1D dilated CNNs (WaveNet‑style) beat handcrafted baselines. A two‑phase hybrid (network early, fast heuristics later) resolves a 1,000× speed gap and yields many theorems previously provable only by humans.
AI-written summary · about
chapters (8)
- 0:00The limits of AI
- 6:15Pattern matching vs reasoning
- 12:45Mathematics as a testbed
- 18:07Premise selection with AI
- 26:21Improving proof search
- 31:54Moving to higher-order logic
- 34:29Conclusion and Q&A
- 37:01Expert audience questions
related talks
24mThe Rise of Reasoning Models
26mTowards a Certified Proof Checker for Deep Neural Network Verification
39mUnlocking reasoning in Large language models
41mTheory of Modern AI: Learning Theoretic, Game Theoretic, and Algorithmic Perspectives
55mTowards Verified Deep Learning
19mLLMs reasoning and agentic capabilities over time
44mAutomated Scientific Discovery Using Insights from Problem Structure
44mBuilding Knowledgeable Machines