Proof Olympiad 2022

Stream: general

[Hunter Monroe]

I propose staging a Lean-based Proof Olympiad in spring 2022, with competition categories for high school students, undergrads, unlimited (including Lean experts), and AI/nonhuman entrants. This might mesh with the proposed course @Daniel Selsam's mentions below, and in any case would require additional introductory material on Lean with sample problems and solutions . In the interim before spring 2022, a training site could host sample problems, provide easily navigated courses (like the Natural Number Game), and track individual progress with a Hall of Fame (Codewars is not sufficiently organized). I have mocked up a landing page. The Olympiad and training site could build on the TUM's Proving for Fun site infrastructure, which TUM is willing to make available as is, although it may be preferable to create a new site allowing web-based entry of answers with immediate feedback, like the Natural Number Game but with a Hall of Fame and user accounts. Large-scale proving contests have previously been proposed by Haslbeck and Wimmer. The TUM has hosted proving contests in parallel with ITP conferences, although not open to the public. That experience suggests that creating the problems is resource intensive. So we would be considering substantial work to create a site, introductory materials, sample problems for training, and the actual problems for a spring 2022 Proof Olympiad. For discussion: would this effort be worth it and are there volunteers to do the work and to provide institutional backing that would likely be required? Should we use the TUM infrastructure (as is with no development possible for now) or create a new site? Should this be based upon Lean 3 or 4?

Daniel Selsam said:

Bowen Liu Several of us in Microsoft are very interested in supporting/developing a polished, universally accessible, advanced-high-school-level, AI-auto-grading proof-based math/cs course on top of Lean. We are just starting to think about possible partners and collaborators.

[Ryan Lahfa]

As a personal pet project with @Julien Marquet we are interested into porting entrance contests of ENS (a French school) into Lean "competitive" games, a version of NNGs where the proof have to be actually sent to a server and type checked and people has to formalize as much as possible stuff.

I'm trying to see how feasible it is to make it trivial to deploy Lean games based on a bunch of Lean definitions on the top of any library.

[Ryan Lahfa]

(the end objective is to train all our colleagues into Lean discovering how fun it is to prove the Dirichlet theorem about primes :-))))))