Feit-Thompson conjecture on primes

Conjecture · feit_thompson_primes

There are no distinct primes $p$ and $q$ such that $\frac{q^p - 1}{q - 1}$ divides $\frac{p^q - 1}{p - 1}$

Formal statement · Lean 4.lean

theorem feit_thompson_primes (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (h : p < q) :
    ¬ (q ^ p - 1) / (q - 1) ∣ (p ^ q - 1) / (p - 1) := by
  sorry

Proof. sorry

Nobody has tried yet.