**On Lean and teaching** Rough notes taken during the panel discussion, Thursday 14 July 2022, ICERM * Patrick M: Using Lean for teaching: for examples see https://www.imo.universite-paris-saclay.fr/~pmassot/enseignement/ and https://www.imo.universite-paris-saclay.fr/~pmassot/mdd154/. Natural language style tactics. Lecture notes displayed as webpage that integrates Lean. Clicking to display tactic state in a proof. Provide a container-ed version that makes it easy to install. * Rob L: Logic and Proof course + online textbook with Jeremy, logic-heavy, discrete math & intro to proof course. As a tool for teaching CS students to learn to write proofs, and in a [formal proof and verification](https://cs.brown.edu/courses/cs1951x/) course at Brown - give them projects to do. Important and helpful to have TA's who know Lean syntax and installation stuff. * Kevin B: An excuse to make computer games at work. [Three courses]() this coming year. 1) Intro to proof course, sets functions and equivalence relations, Lean as an optional part. 2) Graduate level course as workshops to number theorists and algebraic geometers. 3) [Final-year undergraduates](https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/), project based, formalize something you've learned from the pure maths curriculum. * Jeremy A: Students greatly enjoy it. Make sure it's not overwhelming, design exercises in such a way that it can be done, avoid helplessness. * KB: A tricky part is to get the exercises right. For example, you want to avoid type coercions in the beginning. Through trial & error, as a teacher you learn how not to get into the weeds right away while teaching. * PM: For an exercise, provide all the necessary lemmas and definitions. Present it as "naive" type theory. * Heather M: A point & click interface for Coq that was developed for teaching, Edukera. After teaching a bit of Lean, exercise about understanding what the goal state is at a certain moment in a paper proof. * KB: Main feature of Lean that is useful for teaching mathematics: the fact that it displays the tactic state in real time. * KB: Students with programming experience advance more quickly. For students without programming experience, don't judge code quality. * Q: Plagiarism problems? A: don't make the exercises part of the grading. * Q: Creating a course without too much tooling/installation? A: Various options: * Lean Web Editor. * Gitpod -> also Lean 4, and is fast * Bundled version that can be downloaded If you want to create a course using one of these technologies, ask someone who has already done it to find out how. * HM: idea of doing a few demonstrations of Lean in a course that does not use Lean otherwise. * Q: Is it appropriate for weak students? * KB: Yes, sometimes it can even help weaker students. * Matej P: Teaching format in classroom? A: Live-coding demonstration in Lean, with suggestions from the students. * MP: suggested exercises * "scavenger hunt" : finding a lemma in Mathlib. (big challenge) * take an informal definition and write it down formally * JA: good strategy for learning Lean is to teach it to your students. * Thomas B: big step going from tutorials to an actual Mathlib contribution, how to teach that transition? * Anatole: for an undergraduate in math, big advantage of knowing Lean for then later learning to read more informally written mathematics texts: you get past the routine stuff more quickly and you get more quickly to the heart of the matter. * PM: risk that students could do an "automatic" proof without understanding anything. Here the natural language tactic is helpful. Lean forces you to be more careful about your logic, also in your informal proofs. * JA: this is also the power of logic, and teaching logic. * MP: how do you introduce examples in a Lean-based class? * A: This is still difficult. Abstract stuff is nicer for proof assistants than concrete computations. Importance of eventually merging proof assistants with computer algebra systems.