Hacker News Reader

Comment by svat | Hacker News Reader

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)

View on HN

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.

"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.

> 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.

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?

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

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...

Reply on news.ycombinator.com