4 ms·
Do you have formal problems with formal solutions (so, you know the formalization is sufficiently complete) that cannot be found by existing (powerful) comput
by lupire 3y 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?
- 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