Competitive Math Online Judge

Stream: IMO-grand-challenge

[Ansar Azhdarov]

Hi everyone, I'm not sure if this is an appropriate channel for this topic, it's about math olympiads but not so much about AI.

I recently shared this post on Codeforces (competitive programming platform): https://codeforces.com/blog/entry/147825#comments. Here is the TL;DR: "I want to make a competitive math platform where solutions to problems are submitted in Lean and are checked automatically, so we can have online math competitions like on Codeforces. Formalizing solutions in 'real time' is impossible right now, so there will need to be community effort to formalize math olympiad topics in a library." People were quite excited and some wanted to contribute. So if things go well, there might be an influx of Lean users/contributors coming from competitive programming.

Now, I need some help figuring out how to organize this properly. Should I encourage people to contribute to mathlib directly, or have a fork (with a new 'MO' folder?), or have a separate library, or something different? What would be appropriate short-term and long-term solutions? I'm really not an expert in either Lean or math olympiads, but I now have this huge incentive to learn. I would really appreciate any suggestions on how to go about it.

[Jovan Gerbscheid]

When you say "Formalizing solutions in 'real time' is impossible right now", I presume you mean that mathlib doesn't have enough maths olympiad maths to be able to formalize all olympiad problems? If that is the problem, I can see 2 solutions:

• Don't pose problems whose proofs depend on maths that isn't in mathlib.
• Contribute to mathlib in order to add such missing maths.

[Ansar Azhdarov]

Jovan Gerbscheid said:

When you say "Formalizing solutions in 'real time' is impossible right now", I presume you mean that mathlib doesn't have enough maths olympiad maths to be able to formalize all olympiad problems?

I meant that you can't expect one to both come up with solutions and formalize them within the time frame of a contest. For example, with 3 problems in 5 hours. At least, that was my impression. I just looked again at some solutions on Compfiles and many take fewer than 100 lines of non-golfed code, so maybe it is possible if you are skilled enough. I guess I just need formalizing more problems myself.

[Jovan Gerbscheid]

Yes, it is of course much more challenging to solve and formalize a problem within a time limit, compared to only solving it on paper. But that's exactly the challenge, right?

[Alex Meiburg]

I think there's room for designing problems specifically for the format. To show what I mean...

Maybe the question poses a funny inductive type with some funny equivalence relation, and then some question about what structures can emerge; and then the answer ends up being "oh, under this equivalence the type just collapses to be essentially isomorphic to the natural numbers, and then the answer is proved using the fundamental theorem of arithmetic as an easy corollary". So then the work is showing the nice equivalence with Nat, and the "reasoning" part of the proof is just a few lines, and maybe the whole thing is just 30 lines.

That would obviously not make any sense at all as an IMO question, and the 'math-y' part is light, it's a bit closer-to-the-metal in terms of Lean's theory.

[Joseph Myers]

Sometimes when looking at much-easier-than-IMO competition problems, I think they would be awkward to state formally because much of what's involved in a sufficiently easy problem is simply getting a precise understanding of the informal statement, so any formal statement would be most of the way towards a solution.

The suggestion of problems that are close to the Lean theory with little mathematical content (which certainly has merits as a kind of problem enabled by automated marking) seems like a kind of opposite of that issue.

[Ansar Azhdarov]

@Alex Meiburg Thank you for the suggestion! I guess it makes sense if some new categories of problems would emerge, and the kind of what you described could be one of them.

[Ansar Azhdarov]

If anyone is interested, the proof of concept is available here: https://leanoj.org/domjudge/public.