Erdős problem 674

Are there any integer solutions to $x^xy^y=z^z$ with $x,y,z>1$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

674.lean

Retained formal statement1 of 2

Are there any integer solutions to $x^xy^y=z^z$ with $x,y,z>1$ ?

Ko [Ko40] proved there are none if $(x,y)=1$ , but there are in fact infinitely many solutions in general - for example, $x=2^{12}3^6$ , $y = 2^83^8$ , and $z = 2^{11}3^7$ .

FormalConjectures/ErdosProblems/674.leanErdos674.erdos_6741 lineExact file

1True ↔ Erdos674.solutionSet.Nonempty

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.