In this 1 hour and 26 minute seminar from the Harvard CMSA New Technologies in Mathematics series, Google DeepMind researcher Thomas Hubert explores the intersection of reinforcement learning and formal mathematics through AlphaProof. Discover how the digital revolution has transformed mathematical research, from Gauss computing primes by hand to computers tackling Millennium Prize Problems like the Birch and Swinnerton-Dyer conjecture. Learn about the emerging paradigm where computation evolves into reasoning through two key developments: the rise of formal mathematics and machine intelligence. Hubert explains how these advancements are reshaping mathematical research and what role they will play in the future of mathematics.
Overview
Syllabus
Thomas Hubert | AlphaProof: when reinforcement learning meets formal mathematics
Taught by
Harvard CMSA
Related Courses
-
Machine Learning and Theorem Proving in Formal Languages
-
Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification
-
Logic and Formal Methods in Mathematics and Machine Learning
-
Can AI Help with Hard Mathematics? - Applications and Challenges
-
Llemma: An Open Language Model for Mathematics
-
Peano: Learning Formal Mathematical Reasoning Without Human Data
