Two hours of Lean

Stream: Lean for teaching

[Julian Berman]

Hello.

I have a 2 hour seminar / lecture in a few weeks and I am tossing around the idea of doing some Lean. My audience are actually neither mathematicians nor computer scientists, they are graduate students in sort of applied data analysis fields (e.g. industrial engineering and the like), but these seminars are meant to "round out" some of their knowledge and hopefully just be a bit of fun.

I don't know how great of an idea doing Lean is -- certainly I find it interesting, but my intuition says something like the NNG will be playful enough to be interesting to others there as well, especially those who have no experience whatsoever with mathematical reasoning, and I would rather not talk for 2 hours if I could instead do some game-y thing (which obviously the NNG will offer). If anything my thinking is they'll come out of the seminar with "oh cool I can write a program to retrieve stock prices, but somehow I can write one to teach a computer that addition commutes!?"

Does anyone have experience or suggestions for ways to make doing so successful (or care to talk me out of doing this)?

[Kevin Buzzard]

You can spend the first 30 minutes proving 2+2=4. I'm serious.

[Kevin Buzzard]

import tactic

inductive number
| zero : number
| S (n : number) : number

namespace number

def one := S(zero)
def two := S(one)
def three := S(two)
def four := S(three)

-- example : two + two = four -- error because + not defined

def add : number → number → number
| n zero := n
| n (S(d)) := S(add n d)

example : add two two = four := rfl

end number

I do this with schoolkids. I first talk about the definition of nat (0 is a number, S(number) is a number, and that's it) and then I define numbers up to 4 and then I explain what "that's it" means (principle of recursion/induction) and then I spend a lot of time discussing how to define the function which adds 2 to a number and then I define add and then we prove 2+2=4 with a seven line proof which I get them to do (2+2=2+S(1)=S(2+1)=S(2+S(0))=S(S(2+0))=S(S(2))=S(3)=4) and then I show them how Lean can do it with the high-powered rfl AI. You can go on from there to start talking about add_comm (which I would recommend proving before add_assoc because the proof is longer but there are fewer variables around). That would easily take well over an hour if you explain everything from first principles. Then you can go on to some harder stuff and show off some of mathlib. That would fill 2 hours -- you're the one who can tell how appropriate it is but it is one possibility.

[Kevin Buzzard]

The proof of add_comm is very conceptual. It's a common thing in mathematics that sometimes to prove a theorem it first helps to prove some of its corollaries. add_zero and add_succ are axioms, and if addition were commutative then this would imply zero_add and succ_add, so prove them next by induction on the second variable (the second variable is the only thing you have control over at this point), and then try add_comm and you'll find that all the ingredients are there.

[Kevin Buzzard]

Then you have to decide whether to prove stuff about mul or whether to do other things

[Julian Berman]

Thanks Kevin! Certainly I am heavily inspired by seeing some of what you've lectured on. I believe I've seen a video of you following the above -- the thing that drew me towards NNG a bit more than this was simply that it seemed I could perhaps do tutorial world in unison, then an hour through or so pause and let folks try a level or two on their own -- perhaps though a hybrid approach where first something like the above shows lean (and mathlib) off a bit and allows for some explaining, and then we collectively try NNG will meet both needs... I'm trying to basically have some explanation but some collective "try lean yourself" as opposed to just me talking (and I'm slightly worried purely going down this route in a lean file somewhere will not give these folks enough to be able to do so on their own).

[Arthur Paulino]

Hey @Julian Berman, how did it go btw?

[Julian Berman]

Well enough I think. There were some unrelated campus events that day which were a bit distracting to students and made it hard to get a good read on feedback, but yeah I think it went well, I'd try it again

[Julian Berman]

I think varying the bit of math that's used to show lean off would be a good experiment too