Lean Online Judge is an online Math Olympiad platform that makes use of the Lean interactive theorem prover. This means that problems and solutions are written in the special 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 goal of the project is to introduce Lean to the Math Olympiad community to make that happen. A more technical challenge is to develop a specialized Math Olympiad library in Lean. For now, Lean's generic mathematics library Mathlib is being used.
The project is under active development. Join the Discord server to participate in all related discussions.
[LOJ] The logo depicts a person having a moment of enlightenment while solving a Math Olympiad problem.