Erdős problem 674
Are there any integer solutions to with ?
Sources
FormalConjectures/ErdosProblems/
674.lean
Retained formal statement
Are there any integer solutions to with ?
Ko [Ko40] proved there are none if , but there are in fact infinitely many solutions in general - for example, , , and .
True ↔ Erdos674.solutionSet.Nonempty