What is this?
Lean Online Judge is an online Math Olympiad platform that makes use of the Lean proof assistant. This means that problems and solutions are written in the formal syntax of Lean, which enables automated solution checking without human intervention. In particular, this makes it possible to host regular online math competitions similar to how it's done in competitive programming on platforms like Codeforces and AtCoder.
The current challenge is to develop a specialized Math Olympiad library in Lean to allow users write solutions under typical contest time constraints. Currently, Lean's generic mathematics library Mathlib is being used.
You can join the Discord server to participate in all related discussions. Details on the Math Olympiad library will be shared later.
