Yaël Dillies: Maths formalisation in the age of AI: What the working mathematician should know about Lean

Abstract: A decade ago, a couple of mathematicians entreprised to rewrite their corpus in the extremely pedantic Lean programming language to ensure superhuman correctness of mathematical arguments and as a continuation of the Bourbaki philosophy. Now, AI is spitting mathematical breakthroughs on a daily basis, faster than humans can comprehend them.

In this talk, I will survey the ecosystem built around Lean, in particular by the aforementioned pioneer mathematicians, and explain how it will become a key component in the new age of LLM-powered mathematics that lies ahead of us. I will teach a few concrete skills on how to verify for yourself that a purported Lean proof of a theorem you care about is correct, and encourage the audience to bring their laptops to follow along (Unix-based preferably, vscode with the lean4 extension installed would be best).