Project Numina and AI for Theorem Proving

In this 57-minute talk from the Institut des Hautes Etudes Scientifiques (IHES), Yann Fleureau presents Project Numina, which develops open-source, open-dataset AI for mathematics. Learn about Numina's achievements, including winning the AIMO progress prize in 2024 and releasing NuminaMath, the largest open dataset of math problems and solutions. Discover the recently released KiminaProver, a state-of-the-art formal math prover, and explore the past, present, and future developments of Numina along with their AI approaches to theorem proving.