Lean project for high-school students

Stream: Lean for teaching

[Lasse Rempe]

Hello all, I installed Lean and joined the Zulip last year after some conversations with @Kevin Buzzard and @Neil Strickland , but never managed to do anything. But now my postdoc @Bernhard Reinke will be offering a Lean summer project for some A-level students from the University of Liverpool Maths School, so I think it is time to make an attempt to get into Lean. One question that has slightly held me back - and is relevant for the project as well, I think - is Lean 3 or Lean 4? Last year I think the work on porting MathLib to Lean 4 was under way, but still some way off, so in some sense it seemed to make sense to hold off on using Lean 4. Is that still the case, or should we start with Lean 4 straight away? Also, are there resources (in English) specifically useful for school students, beyond Kevin's "Natural Numbers Game"? Thanks, and apologies since probably this has been covered somewhere on here before, and if I was more proficient at navigating Zulip I might be able to find the information myself ...

[Mauricio Collares]

Mathlib is more than 90% ported and will likely be fully ported in less than a month. Starting with Lean 4 is now unconditionally the best approach.

[Mauricio Collares]

https://djvelleman.github.io/HTPIwL/ and https://hrmacbeth.github.io/math2001/ both target Lean 4 and could be used with bright high-school students who have done NNG. By the way, a Lean 4 version of NNG is available at https://adam.math.hhu.de/#/g/hhu-adam/NNG4.

[Mauricio Collares]

One possible snag with recommending Lean 4 now is that the documentation might be a bit confusing before Mathlib is fully ported, but as long as you provide install guidance to the students that should be fine.

[Lasse Rempe]

Thank you! That is great news that mathlib is almost ported. We'll go with Lean 4 on that recommendation!

[Jeremy Avigad]

Mathematics in Lean is also working with Lean 4. The port from Lean 3 was done quickly and some cleanup and improvements are still needed (and in progress), but it should still be usable in its current state.