Formal target: Corpus.Erdos418.erdos_418.variants.odd_noncototient
The **Odd Noncototient Conjecture**: every non-cototient is even.
Exact formal statement
LE.le.{0} (Compl.compl.{0} (Set.ofPred.{0} fun x => Exists.{1} fun n => Eq.{1} (HSub.hSub.{0, 0, 0} n n.totient) x))
(Set.ofPred.{0} fun k => Even.{0} k)This target is a formal statement, not a proof of the problem.
Environment availability: available.