News for hackers. Stuff that matters.

A comment on $10M AI Mathematical Olympiad Prize.

Re:$10M AI Mathematical Olympiad Prize by svat on Monday November 27, 2023 @08:51AM (#38432219)
How does this relate to the "IMO Grand Challenge" https://imo-grand-challenge.github.io/ ? Is this a new name / formalization, with prize money attached, or is it entirely independent? (E.g. I see Kevin Buzzard and Leonardo de Moura listed on both that page and at https://aimoprize.com/supporters)
[ Parent | on HN ]
Re:$10M AI Mathematical Olympiad Prize by dwrensha on Monday November 27, 2023 @09:11AM (#38432403)
The IMO Grand Challenge is "formal to formal" -- a solver is given the problem specified in the Lean programming language, and must produce a solution in Lean. To see more concretely what this setup might look like, check out https://github.com/dwrensha/compfiles.

The AI MO prize is "informal to informal" -- a solver is given a problem in natural language and must produce a solution in natural language.

My belief is that the best way to get to "informal to informal" is to first solve "formal to formal", but not everyone thinks so.

[ Parent | on HN ]
Re:$10M AI Mathematical Olympiad Prize by lupire on Monday November 27, 2023 @11:46AM (#38434561)
"Informal to formal" is harder than "formal to formal". These puzzle problems are quite simple (for computers) if you have a formalization.

"Informal to informal" is so far snake oil.

[ Parent | on HN ]
Re:$10M AI Mathematical Olympiad Prize by dwrensha on Monday November 27, 2023 @11:51AM (#38434623)
> These puzzle problems are quite simple (for computers) if you have a formalization.

That may be true someday, but it's not yet! That's exactly what the IMO Grand Challenge is about, and nobody has gotten close to solving it.

[ Parent | on HN ]
Re:$10M AI Mathematical Olympiad Prize by lupire on Monday November 27, 2023 @12:00PM (#38434769)
Do you have formal problems with formal solutions (so, you know the formalization is sufficiently complete) that cannot be found by existing (powerful) computer search techniques?
[ Parent | on HN ]
Re:$10M AI Mathematical Olympiad Prize by dwrensha on Monday November 27, 2023 @12:25PM (#38435136)
About half of the problems in Compfiles have complete solutions. They are marked by the checkmarks in the list at https://dwrensha.github.io/compfiles/index.html .

As far as I know, based on published systems like LeanDojo [1] and Magnushammer [2], computers today can only solve a small handful of the very easiest of these problems (like maybe Imo1959P1).

[1] https://leandojo.org/

[2] https://arxiv.org/abs/2303.04488

[ Parent | on HN ]
Re:$10M AI Mathematical Olympiad Prize by svat on Tuesday November 28, 2023 @01:04AM (#38442866)
Answering my own question: Alex Gerko (who's behind the $10M prize here) says:

> "It came about as me checking on the status of IMO Grand Challenge (which was launched in 2019 https://imo-grand-challenge.github.io) and deciding that it's time to give this idea a boost"

https://twitter.com/AlexanderGerko/status/172920793662562733...

[ Parent | on HN ]