3 ms·
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.
by dwrensha 3y ago
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 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.
- lupire 3y ago"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.
- dwrensha 3y ago> 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.
- lupire 3y agoDo 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?
- dwrensha 3y agoAbout 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 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/ https://leandojo.org/ [2] https://arxiv.org/abs/2303.04488 https://arxiv.org/abs/2303.04488