Comment by samatman

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