I am interested in teaching and outreach, and often get asked to give talks to schoolkids. I gave one today, to a room full of year 10 kids (aged 14-15), and I showed them Lean. This was the youngest group of students I’ve ever attempted to show Lean to. I decided to show them a proof that 2 + 2 = 4, starting from definitions of 2 and +. However by year 10 the students have not seen induction yet, so I started by showing them parts of a YouTube video with stuff in a line falling over (e.g. dominoes, humans). I then defined the naturals (I called them “numbers”) as an inductive type in Lean, showed how to define recursively the function which adds two to a number, and finally we proved 2 + 2 = 4 by unwrapping the definitions of 2 and + and so on.

I really didn’t know how it was going to go. But, to my relief, when we were doing the big calculation, I asked the audience to fill in the next line for all seven lines, and these kids managed to do it! I was very pleased.

Here are the pdf slides. In the actual talk the text appeared slowly (there were beamer pauses) and there were times when I spent a minute or two talking to the kids about what was going on.

On page 12 of the pdf I say “Let’s go and make some numbers using Lean” and this is what I coded up live. I finish by trying to formalise the statement that 2+2=4 but there’s a problem because although I’ve defined `two`

and `four`

I’ve not yet defined addition. We then go back to the pdf, and on page 15 I return to Lean and define addition like this. Then comes the moment of truth: the calculation on line 16 (which appears line by line in the actual presentation) and which I got them to do. Having made it through, I then showed how Lean could prove it with `rfl`

, and claimed that this was because even though we’d only just taught it numbers it was already an expert in numbers. I then asked the audience what other kinds of maths did they think it was possible to teach Lean and immediately one kid said “all of it”. I agreed. I then made some provocative statements about why people like my daughter should not be forced to learn about cosines, and then asked if there were any questions. The first one was “How do I learn more about this stuff?”. But I did feel that I’d lost plenty of people in the room.

I think that age 14-15 is a little too young for this talk. These kids had self-selected — they were at Imperial for an open day (during a UK school holiday) so were probably interested in science. But I wonder if the material presented here would be a little more suited to kids a little older. I’m giving a couple more school talks in the future, so maybe I’ll find out soon enough.