## Stream: Lean for teaching

### Topic: Lean ideas for smart high school students

#### Kevin Buzzard (Jun 23 2021 at 09:11):

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 (Jun 23 2021 at 09:25):

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 (Jun 23 2021 at 11:27):

@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 (Jun 26 2021 at 01:48):

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.