Hints?

Stream: Lean for teaching

[Yury G. Kudryashov]

Hi, I think about proposing a Lean based course at University of Toronto, and I have a lot of questions:

1. What can be covered in one semester?
2. How an exam can look like? Rules say that the student must earn large part of their grades in supervised settings to prevent cheating, so take home exam "formalize the following proofs" is not an option.

[Kevin Buzzard]

Can you have a project based exam? Some of our courses at Imperial have this

[Andrew Ashworth]

I think a course like this, based on learning Lean, would do better with a final project instead of a final exam. However, if you still need a final exam, you could do a paper one based on type theory + whatever mathematics you cover

[Andrew Ashworth]

From the courses I have seen in CS departments, roughly half the semester is spent getting to grips with the type theory and formal proving, and the other half diving into some topic to be investigated using the tool. Software Foundations might be a good guidebook for the front half of the course, but suitably translated into Lean...

[Yury G. Kudryashov]

I was thinking about a mathematician oriented course with as little type theory as possible.

[Yury G. Kudryashov]

I'll reread the rules next week to see if we can have a final project.

[Patrick Massot]

For my course the final exam happens in a computer room but all exercises should be done in Lean and on paper. I mark both versions.

[Patrick Massot]

Because the stated goal of the course is to improve traditional proof writing skills, but it would feel unfair to spend that much time learning Lean without giving any credit for this.

[Patrick Massot]

The final mark also incorporate things where they can easily cheat (things they are asked to do during the exercise sessions where they are allowed to talk to each others or even at home). For instance next week they will be on vacations but they have five little proofs to work on. They will send me the Lean file as well as handing me a hand-written version for the two most interesting proofs.

[Patrick Massot]

Everything is slow because Lean is complicated and writing proofs on paper is extremely slow. For students there is a huge psychological barrier to taking a piece of paper and a pen in a room filled with computers.

[Patrick Massot]

Last year I started too fast because I underestimated how students didn't understand anything in the previous semester. So I'm currently lecturing this again but, after four weeks, I'm not yet where I expected to be at the end of the first lecture last year. Each session lasts two hours. It starts with explanations on the blackboard (involving no type theory at all) and then they play with Lean. Remember the context: they are first year undergrads that did no proper math in high school, are meant to be above average but not great (although a couple of them are great by accident). They has one semester of calculus where lectures include epsilons but exercises sessions and exams don't. So far I did four weeks:

• Some calculations (this is all they know before coming), first explicitly rewriting using mul_assoc etc. then using calc and then a killer tactic (I have a compute tactic that tries norm_num, ring and abel)
• Implication, iff and conjunction. Proving things like a \le b \iff a+c \le b+c using that a\le b iff 0 \le b-a and computing.
• Finishing the above and some more abstract exercises in using implications and iff: some exercise about variables P Q : Prop instead of actual statement. The master exercise was then proving that, a and b being natural numbers, a |b iff gcd(a,b) a using only reflexivity and antisymetry of divisibility and the fact that c | gcd a b \iff c | a\and c | b (in Lean and on paper)
• Universal quantifier and disjunction (disjunction was not done earlier for lack of time and because I saw last year that it's very complicated for students). Exercises on forall where about even and odd functions, and then increasing and decreasing functions. First exercises on or where all about x*y = 0 iff x = 0 or y= 0. Then exercises mixed both using stuff like x \le y or y < x.

Next time I'll finish the exercises on forall and or and start with exists (probably mostly using divisibility and surjective functions). Then I'll be able to start exercises about limits (that I hoped to do at the end of the first class last year...). Then there will be negations and proofs by contradiction and contrapositive. This will probably take the bulk of the remaining weeks, but I'd like to do proofs by induction at the end. I have 12 weeks only.

[Yury G. Kudryashov]

Thank you @Patrick Massot !