Lean ideas for smart high school students

Stream: Lean for teaching

[Kevin Buzzard]

Inspired by https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/High.20School.20ITP.20Workshop.20Instructor.20Needed/near/243622869 I thought I'd write down some thoughts.

It would be difficult for me to be involved in the delivery of material for this, because the dates are weekends, however I do have experience working with this kind of student and would be happy to talk to anyone who is interested in this job about potential ideas. Some things which would probably work well are (1) a natural-number-game-like thing and (2) a discussion of induction including induction on equality (e.g. https://xenaproject.wordpress.com/2021/04/03/induction-and-inductive-types/ and https://xenaproject.wordpress.com/2021/04/18/induction-on-equality/). Something else which would fit well into this could be an introduction to group theory, up to and including a construction of the Knuth-Bendix confluent rewrite system for group theory a la https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/src/week_2/Part_A_groups.lean , which is a fancy way of saying "make simp solve (a * b) * 1⁻¹⁻¹ * b⁻¹ * (a⁻¹ * a⁻¹⁻¹⁻¹) * a = 1`. Each of these could be run as either one or two sessions I would imagine.

[Monsoon Math Camp]

If each of these are short enough to be two sessions each, we'd welcome multiple mini-workshops too! Then we could have one mini-workshop on each of the three weekends (July 3-4, 10-11, 17-18).

[Koundinya Vajjha]

@Monsoon Math Camp I would be very happy to take this up if no one else took it up just yet. I cannot do it on the July 3-4 weekend though.

[Apurva Nakade]

This is really cool.

Let me shamelessly plug a 5-day, no pre-req class that I and @Jalex Stark taught at Canada/USA Mathcamp. That camp had a very similar audience.
https://apurvanakade.github.io/courses/lean_at_MC2020/index.html
https://github.com/apurvnakade/mc2020-Lean
Please free to use any of the above notes as you see fit.

Unfortunately, these dates are too soon for me to participate. I hope I can help out in a future year.

[Koundinya Vajjha]

@Apurva Nakade thank you for those notes! They look great.