https://mathoverflow.net/q/511601 is a fun little math problem that came up in one of my projects, I didn't have any reason to expect it to be particularly tough, but none of the models I've thrown at it have been able to solve it past a few minor reductions and special cases.
I expect that there is some relatively easy-to-state solution to this problem, but that it's different in form from what most existing proofs and tools yield. Perhaps if I dumped millions of dollars into it an agent might chance on the solution. Or perhaps my luck is such that my fun little problem is truly intractable...