Carmichael's totient function conjecture

Theorem · carchimaelTotient_bound

In Theorem 6 in [F1998], Kevin Ford proves that the smallest counterexample to Carmichael's totient function conjecture must be $≥ 10 ^ (10 ^ 10)$

Formal statement · Lean 4.lean

theorem carchimaelTotient_bound {n : ℕ} (hn : 0 < n) (hn' : n < 10 ^ (10 ^ 10)) :
    CarmichaelTotientFor n := by
  sorry

Proof. sorry

Nobody has tried yet.