New Technologies in Mathematics Seminar

Speaker: Thomas Hubert (Google DeepMind)

Title: AlphaProof: when reinforcement learning meets formal mathematics

Abstract: Galileo, the renowned Italian astronomer, physicist, and mathematician, famously described mathematics as the language of the universe. Progress since only confirmed his intuition as the world we live in can be described with extreme precision with just a few mathematical equations.
In the last 70 years, the rise of computers has also enriched our understanding of and revolutionized the world we live in. Mathematics tremendously benefited from this digital revolution as well: while Gauss had to compute primes by hand, computers and computation are now routinely used in research mathematics and contribute to grand problems like the Birch and Swinnerton-Dyer conjecture, one of the Millennium Prize Problems.
Today, computers are entering a new age, one in which computation can be transformed into reasoning. In this talk, I would like to discuss two such developments that will undoubtedly have an integral role to play in the future of mathematics: the concurrent rise of formal mathematics and of machine intelligence.