def IsCarmichaelNumber (n : ℕ) : Prop

A Carmichael number is a composite natural number n > 1 such that a ^ n = a in ZMod n for every a, i.e. it satisfies the conclusion of Fermat's little theorem despite not being prime.

theorem carmichael_numbers_infinite : {n : ℕ | IsCarmichaelNumber n}.Infinite

There are infinitely many Carmichael numbers; the set {n : ℕ | IsCarmichaelNumber n} is infinite.