Patrick's course

Stream: Lean for teaching

[Kevin Buzzard]

Patrick -- your course is done now, right? This https://www.math.u-psud.fr/~pmassot/enseignement/math114/ is the link I know about -- is there anything else you have to show off? How did it go?

[Scott Morrison]

My French is not so good, so I asked google for some help, and very much liked its translation: "This course uses the Lean Demonstration Wizard".

[Angela Li]

ooo this thread is old but how did this course go?

[Johan Commelin]

@Patrick Massot :up:

[Patrick Massot]

I think it went well, but half of it took place during Covid lockdown, which disrupted everything of course. I think more students got something from it than during the first iteration. And the Lean community got the tutorials project (which is an almost direct translation of the exercises from this course), and one more contributor to mathlib (Anatole Dedecker). It is still frustratingly difficult for student to translate Lean code into normal maths writing, more difficult than writing Lean code. I may try some new things for the next iteration specifically because of this issue.

[Peter Jipsen]

In the Lean Together Panel on teaching with proof assistants Patrick showed a Future slide (51:30 https://youtube.com/watch?v=mTLuON5eRZI&feature=share ) with some amazingly readable Lean code. Is this available or described in more detail somewhere? Seems it would definitely be helpful with using Lean in teaching

[Kevin Buzzard]

I would add that I'm very much looking forward to seeing his attempts at controlled natural language via lean 3 parsers and tricks.

I have been trying to write readable lean code in the formalising mathematics repo

[Patrick Massot]

I have a full set of basic tactics (enough to do the tutorials project) in this controlled natural language but they are in French.

[Scott Morrison]

What is the error reporting like when you step outside the controls?

[Patrick Massot]

This is of course the trickiest part. In the end I gave on certain goodies for the sake of error reporting. Especially tactics that actually try several different tactics are very bad for error reporting because the error that surfaces is typically from the last tactic that was tried whereas the first one would have succeeded without a small typo in the arguments.

[Patrick Massot]

But I don't think students are more confused than with normal tactics, before they are totally unable to read error messages anyway.

[Patrick Massot]

This is not even specific to Lean. I'm still waiting for students who can read basic python error messages.

[Patrick Massot]

Actually I think my error messages are more read than python's messages since I wrote error messages in French.

[Peter Jipsen]

Are the tactics perhaps available somewhere to try out? Or some example files to browse? (No problem if they are in French.) The slide in your presentation made this approach look very useful

[Kevin Buzzard]

Patrick is definitely right about error messages. I am not really a programmer and I still remember how much I'd felt I'd levelled up in lean when it dawned on me that actually trying to understand what the error messages said was really helpful. I still get loads of questions of the form "why doesn't this work"for which the answer is "lean is telling you exactly which variable you put which is wrong, and what you should have put'