Zulip Chat Archive

Stream: Lean for teaching

Topic: Thoma-Iannone paper on teaching with Lean

Kevin Buzzard (Jul 16 2021 at 19:37):


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.

Last updated: Dec 20 2023 at 11:08 UTC