IMO Grand Challenge

Stream: general

[Leonardo de Moura]

https://github.com/IMO-grand-challenge
https://imo-grand-challenge.github.io/

[Johan Commelin]

I think this is a really awesome challenge, and I wish you the best luck! This would be an amazing milestone!

[Kenny Lau]

Maybe the AI would instead find a contradiction in Lean :P

[Daniel Donnelly]

Is there any reward for solving this challenge?

[Leonardo de Moura]

Is there any reward for solving this challenge?

Yes, glory, awards, AI legend status, 7 digit salaries, to cite a few :big_smile:

[Johan Commelin]

@Daniel Donnelly A gold medal?

[Kevin Buzzard]

This question of whether computers could do IMO problems came up at AITP in April and when I heard it I just laughed -- "clearly computers are a million miles from this". However I've been thinking about it more and more recently, we formalised some IMO solutions in a thread herehere and some were very straightforward, there is already an algorithm in Coq for solving geometry problems, and so on. Many Olympiad inequality proofs are very short and ingenious, and Daniel Selsam has suggested to me that they will be accessible to machine learning attacks, and whilst gold is a very very lofty ambition or would not surprise me at all if some lean tactic could get the occasional question out, and that's where these things start.

[Jeremy Avigad]

I just came across this: https://aeon.co/videos/can-you-solve-this-slippery-maths-puzzle-that-doubles-as-a-morality-tale.

[David Shin]

Hi, I would love to contribute towards the IMO Grand Challenge project in some way if possible. Is there a project roadmap or something that I can look at to see if there is some way I could get plugged in? I have no experience with Lean, but am eager to learn about it. I was a former USA IMO team member and currently work as a quantitative developer in finance (experienced in C++ and python).

[Bryan Gin-ge Chen]

Welcome! There's a lot more discussion in the dedicated stream: https://leanprover.zulipchat.com/#narrow/stream/208328-IMO-grand-challenge

[andy]

Kevin Buzzard said:

there is already an algorithm in Coq for solving geometry problems, and so on.

Would love to see this algorithm. @Kevin Buzzard any links? I found GeoCoq, but it is more related to formalization, not proving methods.

[Kevin Buzzard]

Wasn't it called something like the area method? The problem with the naive approach is that it's something like triply exponential but this was better and more limited. I only know about it from online search

[Yaël Dillies]

Here's a link to an article describing the method: https://www.researchgate.net/publication/278775998_The_Area_Method_a_Recapitulation