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