Patrick Massot

Teaching mathematics using Lean

Since 2019, I’m using Lean to teach precise mathematical reasoning to first year undergrads in Orsay. Along the way, I developed Verbose Lean, a set of tools built on top of Lean that offers a syntax that is easier to transfer to paper, and more control on what the software can or cannot do automatically. In this talk I will show what it looks like and emphasize the flexibility it brings to teachers. This flexibility allows to tune the amount of help given to students and the level of precision required from them. Discussion is welcome.