Thoma-Iannone paper on teaching with Lean

Stream: Lean for teaching

[Kevin Buzzard]

https://link.springer.com/article/10.1007/s40753-021-00140-1

A few years ago, when I was far more clueless about what works and what doesn't work with undergraduates and Lean, Athina Thoma watched me give a series of 30 lectures to 1st year undergraduates at Imperial with occasional Lean thrown in. This was back in the days when I was convinced that Lean could help weak students to learn how to do e.g. basic questions about equivalence relations (and before I realised that getting weak students to not only learn the course but also learn a hard programming language was really not a viable way to proceed). Athina went on to write up a paper with Paola Iannone about the experience, and it was published last week.