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 goal of the project is to introduce Lean to the Math Olympiad community and make this possibility a reality. A more technical challenge is to develop a specialized Math Olympiad library in Lean via community effort. Currently, Lean's generic mathematics library Mathlib is being used.
The platform is under active development but is already usable. See How to use it? for more information. You can also join the Discord server to participate in all related discussions. Details on the Math Olympiad library will be shared later.
