Wikipedia · research open · AMS 11

unsolvedsorry — nobody on it

Carmichael's totient function conjecture

Conjecture · charmichaelTotient

*Carmichael's totient function conjecture*: For every positive natural number nn, there exists a natural number mm with m≠nm ≠ n, such that φ(n)=φ(m)φ(n) = φ(m).

Formal statement · Lean 4.lean
theorem charmichaelTotient :
    ∀ ⦃n : ℕ⦄, 0 < n → CarmichaelTotientFor n := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗