class notes, mathcamp 2020

Stream: general

[Jalex Stark]

@Apurva Nakade is teaching a mini-course on Lean for high school students at a math summer camp.
We wrote ahead of time a stock of lean code broken up into small exercises, together with some exposition similar to the beginning of #mil (some of it is directly copied, I think)
https://github.com/jalex-stark/lean-at-MC2020/tree/master/lean_at_mc2020_source/source

Apurva, correct me if I have the details materially wrong:
Apurva has five one-hour class periods, the second of which is today.
He's releasing one chapter of notes at the beginning of each class period. During class he lectures over video chat for some initial segment (taking questions along the way) and then students work on the remaining exercises.

Afterwards, he carves out some chunk of what's written to use for the next day's notes.

[Kevin Buzzard]

How did the first class go Apurva? I'd be really interested to know. This is smart high school kids right? Maybe some of my blog posts or NNG would be of interest to them? They might also be interested in the Xena project discord server, there are some schoolkids hanging out there.

[Kevin Buzzard]

I fixed some trivial typos in a PR

[Kevin Buzzard]

If you expect people to download the project with leanproject get then you shouldn't have a leanpkg.path, you should have a .gitignore, and you shouldn't have a _target directory. If you don't expect people to download it then I guess none of this matters.

[Apurva Nakade]

There roughly 22-23 students in my class right now. It is going pretty well. Day 1 was a little rough as most students are new to functional programming. But Day 2 was much better. They all did the problems much faster than I expected :D I ended up having to add more problems than to remove some!

[Apurva Nakade]

Many students have been doing the NNG simultaneously.

[Apurva Nakade]

I did give links to your blog, discord sever, and even your twitch channel to them.

[Apurva Nakade]

Unfortunately, because of the camp being online it is hard to gauge precisely what's happening on the students' end. But next week I and Jalex are planning on meeting them for potential projects, fingers crossed!

[Kevin Buzzard]

Life is a bit chaotic right now so as you say it's very difficult to judge how well people are doing, but it sounds like you've had a great success today Apurva. Well done for taking this on! At the end of it, I would be really interested to know details of what you felt went well and what you felt went badly.

[Apurva Nakade]

There's a camper here who finished the NNG in three days xD

[Kevin Buzzard]

If they've figured out how to install lean and mathlib, tell them to clone the project and do the lost levels :-)

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world10/level18q.lean

[Apurva Nakade]

The course went quite well in the end! We have 3-4 campers who want to do projects now

[Apurva Nakade]

There were actually a lot of campers who found this very interesting, but I think I did not manage to convince all of them that this is "serious math" xD
But many loved Lean as a fun game

[Apurva Nakade]

Also, here are the notes I used for the class: https://apurvanakade.github.io/courses/lean_at_MC2020/index.html
Still need to tidy them up a bit

[Apurva Nakade]

If I teach this again, I might teach a math topic (I'm thinking category theory/point-set topology) using Lean, instead of teaching Lean as its own thing.

[Kevin Buzzard]

If these are high school kids then one option is a basic theory of sequences and limits -- Patrick (especially), myself and others have spent quite some time thinking about how to do this, and by next year you'll have the real number game to look at.

[Kevin Buzzard]

For point set topology, you can prove stuff like continuous image of compact is compact, or compact subspace of Hausdorff space is closed, in a fairly natural way, once you have taught people how to handle sets, functions etc, and have also taught them the basics of topology ie def of top space and cts fn

[Jalex Stark]

we have the source for the notes at https://github.com/jalex-stark/lean-at-MC2020
we're able to build manually and deploy the html to a website, but we don't know how to make it so that when you open the project in VSCode, you get a nice display in the documentation tab

[Bryan Gin-ge Chen]

I believe you just need to put the HTML files in a directory called html/

[Apurva Nakade]

Kevin Buzzard said:

If these are high school kids then one option is a basic theory of sequences and limits -- Patrick (especially), myself and others have spent quite some time thinking about how to do this, and by next year you'll have the real number game to look at.

This is really cool. Epsilon-delta proofs are usually so dry to teach. Teaching them through coding would actually make them interesting to learn.

[Aaron Anderson]

Updated 2022 version of these notes: https://awainverse.github.io/mc2022-Lean