Zulip Chat Archive

Stream: Lean for teaching

Topic: Patrick's course

Kevin Buzzard (May 19 2019 at 20:34):

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 (May 20 2019 at 00:20):

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 (Jan 02 2021 at 16:20):

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

Johan Commelin (Jan 02 2021 at 17:16):

@Patrick Massot :up:

Patrick Massot (Jan 02 2021 at 18:19):

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 (Mar 15 2021 at 17:29):

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 (Mar 15 2021 at 22:38):

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 (Mar 15 2021 at 22:39):

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 (Mar 15 2021 at 23:12):

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

Patrick Massot (Mar 15 2021 at 23:15):

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 (Mar 15 2021 at 23:15):

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 (Mar 15 2021 at 23:16):

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

Patrick Massot (Mar 15 2021 at 23:16):

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

Peter Jipsen (Mar 16 2021 at 05:26):

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 (Mar 16 2021 at 06:40):

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'

Last updated: Dec 20 2023 at 11:08 UTC