Hi Codeforces!

Almost a year ago, I wrote a short blog post asking whether it is possible to host online math competitions in a style similar to Codeforces. The main requirement for the platform I envision is that it should be proof-based (as a competitive math platform) AND support automated submission checking (as an online judge). While there are awesome projects like Project Euler and MathDash, to the best of my knowledge, none of the existing platforms fulfill this specific requirement.

The proposal I had was to use so called proof assistants such as Lean that allow one to type in mathematical proofs in a formal language and automatically check their correctness. The original question asked whether these systems were mature enough for the task. Since then I learned that they are mature enough for way more than that. In particular, Lean has been used to formalize contemporary research-level mathematics [1, 2].

Now, it's not as ideal as it may seem. Lean's mathematics library Mathlib is meant to be used for advanced mathematics and it strives for extremely high generality. For this and other reasons, it is highly non-trivial to use in general, and essentially impossible in the contest environment, where solutions have to be written "in real time". One could develop a new library in Lean, specifically for competitive math, but this is a huge undertaking for a single person, and with my limited experience with Lean, the whole idea kind of staled.