Formal target: Corpus.WikipediaPollocksConjecture.pollock_tetrahedral

Pollock's (tetrahedral numbers) conjecture: every integer is the sum of at most $5$ tetrahedral numbers.

Exact formal statement

∀ (N : Nat),
  Exists.{1} fun f =>
    Eq.{1} N (Finset.sum.{0, 0} Finset.univ.{0} fun i => Corpus.WikipediaPollocksConjecture.tetrahedral (f i))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record