## Stream: general

### Topic: class notes, mathcamp 2020

#### Jalex Stark (Jul 07 2020 at 14:00):

@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 (Jul 07 2020 at 17:13):

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 (Jul 07 2020 at 17:14):

I fixed some trivial typos in a PR

#### Kevin Buzzard (Jul 07 2020 at 17:16):

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 (Jul 07 2020 at 19:24):

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 (Jul 07 2020 at 19:24):

Many students have been doing the NNG simultaneously.

#### Apurva Nakade (Jul 07 2020 at 19:27):

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 (Jul 07 2020 at 19:38):

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 (Jul 08 2020 at 21:42):

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

#### Kevin Buzzard (Jul 08 2020 at 22:33):

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

#### Kevin Buzzard (Jul 08 2020 at 22:35):

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

#### Apurva Nakade (Jul 15 2020 at 15:11):

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

#### Apurva Nakade (Jul 15 2020 at 15:12):

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 (Jul 15 2020 at 15:13):

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 (Jul 15 2020 at 15:16):

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 (Jul 15 2020 at 17:10):

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 (Jul 15 2020 at 17:12):

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 (Jul 16 2020 at 00:40):

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 (Jul 16 2020 at 00:42):

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

#### Apurva Nakade (Jul 16 2020 at 02:12):

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.

Last updated: May 13 2021 at 21:12 UTC