From Theorem Proving to Disproving: Modern Machine Learning versus Classical Heuristic Search

Watch a research lecture from Google DeepMind Montreal researchers exploring the intersection of machine learning and classical methods in automated theorem proving and extremal graph theory. Learn how hindsight experience replay from reinforcement learning was adapted to improve automated theorem proving, achieving results that compete with state-of-the-art heuristic-based provers while generating shorter proofs. Discover the application of AlphaZero and tabu search methods to an Erdős conjecture in extremal graph theory, where curriculum-based approaches led to improved lower bounds for graphs maximizing edges without specific cycle patterns. Presented at the CMSA Mathematics and Machine Learning Closing Workshop, the talk covers research published at ICML 2022 and IJCAI 2024, demonstrating both the potential and limitations of machine learning approaches compared to classical methods in mathematical problem-solving.