Abstract

In the fall of 2024, a collection of masters and PhD students, post-docs and professors got together to learn about Lean and formalizing mathematics. This led to an effort to formalize a theorem of Monsky that there exist no odd dissections of a square by equal-area triangles, which was finally completed last month. In this talk I'd like to reflect on the journey as well as take the opportunity to do some live basic Lean coding (there is nothing to install and all you'll need is an internet connection if you'd like to bring your laptop and code along with me!).