UPDATE: (See the original project announcement below)
It took some time but the proof of concept is now online (hooray!): https://leanoj.org/. You can register and give some of the problems a try. As an example, here is a solution to problem C:
There are many high-quality resources on different aspects of Lean you can find here. The first few chapters of 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 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!
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 (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 and MathDash, 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 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 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!
Auto comment: topic has been updated by paxaq (previous revision, new revision, compare).
Short update: I adapted DOMjudge (standard system to run programming contests) for math contests using Lean. It will be put online soon. Stay tuned!
What about starting with a very limited set of domains (for example, Euclidian Geometry)?
Yes, the plan is to start with number theory or combinatorics since these are easier to formalize. Geometry might actually be the hardest one.
I hardly know anything about this, but is your plan using some sort of fine tuned large language model to translate a 'written proof' to something Lean understands and use this to validate its correctness?
Doesn't necessarily have to be super robust, you could have 'implementation' that requires the human proof writer to structure their proof in a particular format, maybe clearly labelling their lemmas and building a DAG of sorts with them.
Because if this actually ever happens, that would be incredibly cool.
For now the plan is that proofs are written directly in Lean. Just like in normal programming contests, you come up with an intuitive algorithm and then implement it in, say, C++, here you would come up with an intuitive proof and then implement it in Lean. It's just a special kind of programming language.
For that to work, of course, people would need to know how to program in Lean. There are resources for that, but I'm also planning to make tutorials specifically for competitive math. Haven't decided on the details yet though.
That's interesting. Last I checked (and as you mentioned), Lean was pretty cumbersone to use though for any real world proofs, right? What's your plan for that? I suppose the tutorials will help, but do you think that's enough?
Also, in programming, one could 'argue' that your task is to code as well (well, it's really self evident). That's why the 'coding in C++' part is justifiable. Of course I get that you need some way of checking peoples' work regardless of the discipline, but it is still going to be somewhat of a paradigm change for math enthusiasts to not write their proofs in words anymore.
Or maybe not, since a lot of people on Codeforces are also math enthusiasts and I'm underestimating adaptibility.
I've done some formalization including math olympiad problems. It's non-trivial, indeed, and formalizing a proof often takes more time than coming up with the proof in the first place. The great thing is that formalization is a lot of fun once you get the hang of it (even somewhat addictive). So maybe it's okay if at first there is more formalization than math itself, so long as it's fun.
In the long term, enriching mathlib (Lean math library) would be a solution. You see, Lean is not somehow intrinsically cumbersome. It's just that often basic lemmas and theorems your proof relies on are missing from the library, so you have to prove them from scratch. But the library is open source and anyone can contribute. So it really depends on the community. My hope is that competitive math community can fill in the parts that are used in, well, competitive math. I mention having a separate library in the post, but maybe just contributing to mathlib is a better solution.
Regarding the paradigm shift, it's sort of happening in research mathematics as well, albeit very slowly. I believe contestants, presumably mostly high-school students, will only benefit from learning how to formalize their proofs using these systems early on.
Very cool idea. Interested to see what happens.
Thanks!
Great Idea! Good Luck.
Hello paxaq. I have previously thought of the same exact ideas before, but I have never had the time and/or opportunity to start working on such a project and/or take serious steps toward it.
I'm happy to hear that someone started taking such steps, and I'd like to be a part of the initiative.
Awesome! I will definitely need some help at some point. Will let you know.
I'm looking forward to a project like this, and would love to be involved in its development. Let's create a channel to discuss about it, Discord or Telegram.
Good idea! I'll try to organize something.
Any progess? I want to have a look. =)
Oh, I just meant something for the two people who wanted to join the development. Maybe later we can make something for people who want to follow the progress in general, but there's really not much to share at this point)
nice idea! I will try it out once it's ready. I've been wanting to learn lean for a while.
Great Idea! Good Luck.
Auto comment: topic has been updated by paxaq (previous revision, new revision, compare).
Auto comment: topic has been updated by paxaq (previous revision, new revision, compare).
orz
but u have to learn lean... can u just like maybe add a latex editor or smth like MathQuill to make a bit easier so then people can check the lean afterwards if said wrong?
What would you expect to see in the latex editor exactly? I should be able to add feedback on the submission, so that you can see if the solution fails because it doesn't compile or you're solving the wrong problem, etc. If the solution doesn't compile, you should be able to see exactly what the issue is in your Lean editor. You probably want to install Lean, but there is also web app you can use just to try it out.
ok nvm i dont know lean that much but it might make it quicker instead of typing lean to just type lines of latex, but like a dropdown with what ur doing in that line like maybe just to make it easier, cuz then it'll 'translate' to lean
Auto comment: topic has been updated by paxaq (previous revision, new revision, compare).
I had the exact same idea, and got this recommended. Cool!
Auto comment: topic has been updated by paxaq (previous revision, new revision, compare).
A little advertisement for my Lean4OJ:
Lean4OJ is the first online judge in China that specialized using the Lean4 theorem proof assistant, aims to promote various applications of the Lean4 formal language, not limited to mathematics and computer science in AI era.
The main difference from the original poster is that Lean4OJ tries to make full use of Lean's abilities, not limited to MO (Math Olympiad). For example, we have IMO problems, Functional programming problems, Program formal verifications, etc.
Currently, Lean4OJ's problemset contains all problems of CCF theorem proving competition 2025 (lit. CCF 第一届定理证明竞赛) and it is worth submit.
Lean4OJ also allows user to submit modules / libraries (i.e., multiple files), to make environment modularize and reusable.
Lean4OJ is open source: Frontend Backend.
Welcome everyone to visit Lean4OJ and enjoy a happy formalizing day :)
Maybe just to highlight the difference: my focus is on Math Olympiads indeed. In particular, building a specialized MO library or implementing an alternative solution to make live contests possible is the central part of the project. Also, I considered using multiple proof assistants like there are multiple languages on Codeforces, but this is a question for the (probably quite far) future.
BTW you can check Math Jack too! It holds quality contests.