Formal target: Corpus.WikipediaCarmichaelTotient.charmichaelTotient

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

Exact formal statement

∀ ⦃n : Nat⦄, LT.lt.{0} 0 n → Corpus.WikipediaCarmichaelTotient.CarmichaelTotientFor n

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record