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 , there exists a natural number with , such that .
Formal statement · Lean 4.lean
theorem charmichaelTotient :
∀ ⦃n : ℕ⦄, 0 < n → CarmichaelTotientFor n := by
sorryProof. sorry
Nobody has tried yet.