4 ms·
> 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 G
by 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