Can an AI prover solve open problems in mathematics? In particular, problems that are currently beyond the reach of mathematicians? This talk explores this question from the angle of formal mathematics. We will review recent advances in automated theorem provers, and we will the discuss the links with recent progress in software verification frameworks for imperative programs.

Amaury Hayat is a full professor at Ecole nationale des Ponts et Chaussées - Institut Polytechnique de Paris and a member of the Korean Institute for Advanced Studies. He obtained his PhD in 2019 at Sorbonne University. He holds the Hi!Paris DESCARTES Chair, focusing on AI model design for mathematical research. He received the L.E. Rivot Medal from the French Academy of Sciences in 2014, the European Embedded Control Institute PhD Prize in 2019, and the Solemn Prize from the Chancellery of the universities of Paris in 2020. In 2021, he was listed among the Forbes 30 under 30 for Europe.