Formal target: Corpus.PaperKurepa.kurepa_conjecture

Kurepa's conjecture For all $n$, $$!n\not\equiv 0 \mod n$$ This appears as B44 "Sums of factorials." in Unsolved Problems in Number Theory by *Richard K.

Exact formal statement

∀ (n : Nat), LT.lt.{0} 2 n → Ne.{1} (HMod.hMod.{0, 0, 0} (Corpus.PaperKurepa.left_factorial n) n) 0

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record