Hacker News new | ask | show | jobs
by dwrensha 928 days 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.
1 comments
lupire 928 days ago
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?
link
dwrensha 928 days ago
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

link