> COUNTEREXAMPLE TO EULER'S CONJECTURE ON SUMS OF LIKE POWERS
> BY L. J. LANDER AND T. R. PARKIN
> A direct search on the CDC 6600 yielded:
27⁵ + 84⁵ + 110⁵ + 133⁵ = 144⁵
> as the smallest instance in which four fifth powers sum to a fifth
power. This is a counterexample to a conjecture by Euler that at
least n nth powers are required to sum to an nth power, n>2.https://www.ams.org/journals/bull/1966-72-06/S0002-9904-1966...
It is a conjecture whether grinding it out on Lean is a difference in kind, rather than degree. I say degree. But it remains to be seen.