Programming challenge site for lean4

Question

I recently discovered that Codewars supports lean language.

https://www.codewars.com/

However, lean4 does not seem to be supported.

Do you know of any programming challenge sites that support lean4?

---

UPDATE: What I expect from a programming challenge site is that there is a competition aspect.

Answer 1

This is hard to answer since I don't know what you are trying to get out of CodeWars.

Maybe the two closest things right now are the following:

• Natural Number Game (Lean 4 version). This is a level-based tutorial on proofs in Lean, that is a good starting point for anyone wanting to dip their feet in Lean. It is game-like and entirely in the browser.
• Glimpse of Lean tutorial. This is a quick tutorial on proofs in Lean with lots of exercises. Either you can install Lean locally or run it on Github Codespaces (for which they provide a link).

I found these two resources on Learning Lean 4. This page also has a number of tutorials for Lean which are a bit longer, but also more in depth. Many of those have exercises, and Mathematics in Lean also has instructions on how to do the exercises online in Gitpod.

If you are worried about knowing whether your proof is correct, then unlike regular programming, it is very simple in theorem proving: If Lean says your proof is correct, it is correct. You don't need a system on top of Lean to tell you that. So any set of problems for Lean (like in the tutorials mentioned above) is a good set of practice problems.

If you want to avoid installing Lean locally, then you can play with Lean in your browser at https://lean.math.hhu.de/. It can be a bit slow and unreliable, so I wouldn't use it for too much, but it is the quickest starting point. A more reliable solution is Gitpod or Github Codespaces, but I also don't know much about either (but see above for where other tutorials use them). Also, if you own a computer, Installing Lean 4 is not usually that difficult.

Also, Lean 4 is a programming language (not unlike other functional programming languages like OCaml, Haskell, Scala, or Idris). Once you become comfortable with Lean 4 as a programming language, say through the Functional Programming in Lean 4 book, a lot of people like to use Advent of Code as a way to learn and practice programming in Lean 4. Unlike CodeWars, you do the problem locally, and then submit the answer (usually a number) to the website for verification, giving you access to the next level, so it can be used with any programming language.