Informalisation for teaching

Stream: Lean for teaching

[Xander Mackay]

Have any teachers used Lean to improve a mathematics course, without requiring the students themselves to learn Lean? I'm interested in how Lean might be used to improve a maths course while keeping it accessible to students with zero programming experience.

@Jeremy Avigad's "Mathematics and the formal turn" and @Patrick Massot's "Why formalize mathematics?" both mention the possibility of providing proofs where the reader can choose the level of detail, which could be great for students. @Kyle Miller's website contains some info and demos of a prototype of "informalization", but I gather the code hasn't been released yet.

I know there have been maths courses that teach Lean, but informalisation opens up the possibility of using Lean/mathlib in a more unobtrusive way, eg for generating/checking course notes.

I'm thinking of hacking together something along these lines myself. Are there any similar prototypes/ideas I should take a look at first?

[Kevin Buzzard]

I've used lean in a course to go through occasional proofs which I thought were nice to do in lean. I didn't introduce the software at all or talk about tactics, I just discussed how the infoview was changing as I typed more gobbledegook. I did short sessions in several classes and told people that if they had no idea what was going on then they could just read the proof in the printed notes.

[Patrick Massot]

This is definitely a target of the Informal Lean project, but unfortunately this project does not move as much as we would like.

[Patrick Massot]

About Kevin’s idea, you can also use the Verbose Lean library so that what is written in the proof script is also readable.

[Xander Mackay]

Patrick Massot said:

This is definitely a target of the Informal Lean project, but unfortunately this project does not move as much as we would like.

Where is this project, and how do I join? I want to help make it move!

[Patrick Massot]

It is not yet ready for external contribution. Unfortunately Kyle and I are always overwhelmed by other tasks and we didn’t manage to reach the point where we want external contributions.

[Xander Mackay]

Fair, I figured that might be the case. (Something something Mythical Man-Month, Brooks's law, etc.) I'll hack away at something similar myself, and see if I end up with anything worth sharing.