Zulip Chat Archive

Stream: general

Topic: class notes, mathcamp 2020


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 07 2020 at 17:14):

I fixed some trivial typos in a PR

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Apurva Nakade (Jul 07 2020 at 19:24):

Many students have been doing the NNG simultaneously.

view this post on Zulip Apurva Nakade (Jul 07 2020 at 19:25):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Apurva Nakade (Jul 08 2020 at 21:42):

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

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Jul 08 2020 at 22:35):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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/

view this post on Zulip 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