lean tutorial for motivated 8th graders

Stream: Lean for teaching

[Abhishek Anand]

(asking for a friend) is there a lean tutorial aimed at self-motivated younger newbies like 8th graders? Maybe that is too early. But many schools introduce programming as early as 6th grade (my school in India did), so I don't see why Lean cannot be introduced at 8th grade to help solidify mathematical understanding. for example, some of the "solve for x equational problems" that 8th graders solve can be formalized in Lean.

[Kevin Buzzard]

How does the natural number game go down with a self-motivated 8th grader? I don't usually go that low but I wonder whether the tutorial level would be fine

[Kevin Buzzard]

Another alternative is Heather Macbeth's "the mechanics of proof" https://hrmacbeth.github.io/math2001/ . That has a bunch of "solve for x equational problems" at the start.

[Abhishek Anand]

Thanks. I will pass these on. Also, something like NNG for 8th-grade-level geometry, with a tool to visualize the hypotheses would be great.

[Kevin Buzzard]

Yes I totally agree, in the UK we teach so-called "circle theorems" to what we call year 9 kids, I would love to make a geometry game where you can click on points and angles and then invoke theorems but it's basically a very big project which will need expertise in several areas

[Kevin Buzzard]

And I've kind of got my hands full with some polynomial equation for the next 4.5 years

[Luigi Massacci]

@Abhishek Anand you may want to take a look at GeoLogic