Isabel Dahlgren: Lean for the Working Mathematician (for KTH)

Abstract: Two years ago, formalising elementary statements in Lean used to be rather tedious. Today, we can formalise much research-level mathematics with a basic AI subscription. This creates new use cases of Lean, making it a practical tool for the working mathematician. I will begin with an introduction to Lean, Mathlib and related tools (Palomar, TauCeti, Verso), and then discuss possible ways to use Lean for research. No prior Lean experience will be assumed.

Welcome! (This event is targeting people at KTH. SU will have similar seminar separately.)