Zulip Chat Archive

Stream: general

Topic: IMO Grand Challenge


Leonardo de Moura (Sep 07 2019 at 00:12):

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

Johan Commelin (Sep 07 2019 at 07:31):

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

Kenny Lau (Sep 07 2019 at 07:38):

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

Daniel Donnelly (Sep 07 2019 at 14:20):

Is there any reward for solving this challenge?

Leonardo de Moura (Sep 07 2019 at 14:38):

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 (Sep 07 2019 at 14:42):

@Daniel Donnelly A gold medal?

Kevin Buzzard (Sep 07 2019 at 17:36):

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 (Sep 20 2019 at 14:01):

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

David Shin (Sep 24 2020 at 02:40):

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 (Sep 24 2020 at 02:47):

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

andy (May 09 2023 at 04:09):

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 (May 09 2023 at 07:26):

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 (May 09 2023 at 07:54):

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


Last updated: Dec 20 2023 at 11:08 UTC