Hi Codeforces!↵
↵
Almost a year ago, I wrote a short [blog post](https://mirror.codeforces.com/blog/entry/136276) 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_ (since it is a competitive math platform) AND support _automated_ submission checking (since it is an online judge). While there are awesome projects like [Project Euler](https://projecteuler.net/) and [MathDash](https://mathdash.com/lobby), to the best of my knowledge, none of the existing platforms fulfill both parts of this requirement.↵
↵
The proposal I had was to use so called proof assistants such as [Lean](https://lean-lang.org/) 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](https://github.com/leanprover-community/lean-liquid), [2](https://github.com/teorth/pfr)]!↵
↵
_Now, it's not as ideal as it may seem..._↵
↵
Lean's mathematics library [Mathlib](https://github.com/leanprover-community/mathlib4?tab=readme-ov-file) is meant to be used for advanced math and it strives for extremely high level of generality. For this and other reasons, formalizing proofs is highly non-trivial in general, and formalizing solutions in a contest environment in "real time" is practically impossible. One could develop a specialized Lean library 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 stalled.↵
↵
_Well, if no one does it, it will never happen..._↵
↵
I still believe such a platform would be a major boost to both competitive math and proof assistant communities. For now, I am planning to build an online judge using Mathlib ignoring previously mentioned concerns. If things go well and there are enough people interested, the new competitive math library could then become a community-driven project (just like Mathlib), making the goal much more feasible. I'm writing this post mainly to hold myself accountable but if you have any ideas or suggestions, please, feel free to share.↵
↵
I will write a new post when there is some progress to share. Thank you!↵
↵
**UPD:** ↵
It took some time but the proof of concept is now online (hooray!): [https://leanoj.org/domjudge/public](https://leanoj.org/domjudge/public). You can register and give some of the problems a try. As an example, here is a solution to problem C:↵
↵
<spoiler summary="">↵
~~~~~↵
import Mathlib.Algebra.Ring.Parity↵
↵
theorem solution (k : ℕ) (hk : Even k) : 2 ∣ 3 ^ k + 1 ∧ ¬ 4 ∣ (3 ^ k + 1) := by↵
rw [even_iff_exists_two_mul] at hk↵
obtain ⟨n, hn⟩ := hk↵
rw [hn]↵
constructor↵
· simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.pow_mod]↵
· simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, pow_mul, Nat.pow_mod]↵
~~~~~↵
</spoiler>↵
↵
There are many high-quality resources on different aspects of Lean you can find [here](https://lean-lang.org/learn/). The first few chapters of [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) should be enough to get started. I am also planning to make tutorials on Lean specifically for competitive math. If you are experienced in Lean or in competitive math and want to help, please, let me know.↵
↵
I created a [Discord server](https://discord.gg/yhM2TApp) that everyone is welcome to join! This can be used to discuss anything related to the project, Lean, and math olympiads. Future updates will also be made there. Cheers!
↵
Almost a year ago, I wrote a short [blog post](https://mirror.codeforces.com/blog/entry/136276) 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_ (since it is a competitive math platform) AND support _automated_ submission checking (since it is an online judge). While there are awesome projects like [Project Euler](https://projecteuler.net/) and [MathDash](https://mathdash.com/lobby), to the best of my knowledge, none of the existing platforms fulfill both parts of this requirement.↵
↵
The proposal I had was to use so called proof assistants such as [Lean](https://lean-lang.org/) 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](https://github.com/leanprover-community/lean-liquid), [2](https://github.com/teorth/pfr)]!↵
↵
_Now, it's not as ideal as it may seem..._↵
↵
Lean's mathematics library [Mathlib](https://github.com/leanprover-community/mathlib4?tab=readme-ov-file) is meant to be used for advanced math and it strives for extremely high level of generality. For this and other reasons, formalizing proofs is highly non-trivial in general, and formalizing solutions in a contest environment in "real time" is practically impossible. One could develop a specialized Lean library 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 stalled.↵
↵
_Well, if no one does it, it will never happen..._↵
↵
I still believe such a platform would be a major boost to both competitive math and proof assistant communities. For now, I am planning to build an online judge using Mathlib ignoring previously mentioned concerns. If things go well and there are enough people interested, the new competitive math library could then become a community-driven project (just like Mathlib), making the goal much more feasible. I'm writing this post mainly to hold myself accountable but if you have any ideas or suggestions, please, feel free to share.↵
↵
I will write a new post when there is some progress to share. Thank you!↵
↵
**UPD:** ↵
It took some time but the proof of concept is now online (hooray!): [https://leanoj.org/domjudge/public](https://leanoj.org/domjudge/public). You can register and give some of the problems a try. As an example, here is a solution to problem C:↵
↵
<spoiler summary="">↵
~~~~~↵
import Mathlib.Algebra.Ring.Parity↵
↵
theorem solution (k : ℕ) (hk : Even k) : 2 ∣ 3 ^ k + 1 ∧ ¬ 4 ∣ (3 ^ k + 1) := by↵
rw [even_iff_exists_two_mul] at hk↵
obtain ⟨n, hn⟩ := hk↵
rw [hn]↵
constructor↵
· simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.pow_mod]↵
· simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, pow_mul, Nat.pow_mod]↵
~~~~~↵
</spoiler>↵
↵
There are many high-quality resources on different aspects of Lean you can find [here](https://lean-lang.org/learn/). The first few chapters of [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) should be enough to get started. I am also planning to make tutorials on Lean specifically for competitive math. If you are experienced in Lean or in competitive math and want to help, please, let me know.↵
↵
I created a [Discord server](https://discord.gg/yhM2TApp) that everyone is welcome to join! This can be used to discuss anything related to the project, Lean, and math olympiads. Future updates will also be made there. Cheers!
