experiment on students

Stream: general

[Patrick Massot]

Like Kevin, I decided to jump the gun and teach students how to write crappy Lean code like professional mathematicians. This morning I showed Lean to the head of the Maths-CS double major program at Orsay. She was very excited and I will probably get about twenty first year undergraduate students to experiment on during the spring semester next year.

[Patrick Massot]

FYI, the file I used is at https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/demo.lean it only depends on https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/choice.lean (and mathlib of course)

[Patrick Massot]

Of course it's focused on very explicit inefficient tactic mode, not code golf

[Kevin Buzzard]

Having undergraduates to experiment on is really good fun. It's all about the interface, with them. I will be paying particular attention to what my undergraduates struggle with and my guess is that most of the time their struggles will be because they can do something in maths but not in Lean. Ideally the Lean proof should look as mathematical as possible.

[Patrick Massot]

I must say part of my plan is to use whatever insight and documentation you will continue to accumulate

[Johan Commelin]

You even managed to squeeze some French into the demo! Bonus points (-;

[Simon Hudon]

How valuable would it be to have (some) tutorials in video format? I'm wondering if it would be worth looking into doing that kind of presentation

[Patrick Massot]

I think videos could be nice. We could also have semi-interactive web pages with Lean code you could navigate and see the Lean status corresponding to each line, precomputed, not computed in real time. This should be a very easy exercise in using Lean in server mode.

[Kevin Buzzard]

I'm actually making a video in a couple of weeks, it was going to be a general one on dependent type theory. We have a bunch of fancy video-making kit at my university and some people are keen for me to try it out.