Pollock's (tetrahedral numbers) conjecture

Every positive integer is the sum of at most 5 tetrahedral numbers.

References:

• Wikipedia
• A797
• L. E. Dickson, History of the Theory of Numbers, Vol. II: Diophantine Analysis, Dover (2005), pp. 22–23
• Frederick Pollock, On the extension of the principle of Fermat's theorem on the polygonal numbers to the higher order of series whose ultimate differences are constant, Abstracts of the Papers Communicated to the Royal Society of London 5 (1850), 922–924
• H. E. Salzer and N. Levine, Table of integers not exceeding 100000 that are not expressible as the sum of four tetrahedral numbers, Math. Comp. 12 (1958), 141–144
• MathWorld: Pollock's Conjecture

Definitions

def PollocksConjecture.tetrahedral (n : ℕ) : ℕ

The $n$-th tetrahedral number: $T_n = \frac{n(n+1)(n+2)}{6}$.

Equations

• PollocksConjecture.tetrahedral n = n * (n + 1) * (n + 2) / 6

Auxiliary definition

def PollocksConjecture.NotSumOfFourTetrahedral : Set ℕ

The set of natural numbers that are not a sum of $4$ tetrahedral numbers.

Equations

• PollocksConjecture.NotSumOfFourTetrahedral = {N : ℕ | ∀ (f : Fin 4 → ℕ), N ≠ ∑ i : Fin 4, PollocksConjecture.tetrahedral (f i)}

Statements

theorem PollocksConjecture.pollock_tetrahedral (N : ℕ) : ∃ (f : Fin 5 → ℕ), N = ∑ i : Fin 5, tetrahedral (f i)

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

theorem PollocksConjecture.pollock_tetrahedral.salzer_levine : IsGreatest NotSumOfFourTetrahedral 343867

Salzer–Levine strengthening (as stated on Wikipedia/OEIS): there are exactly $241$ integers that are not a sum of $4$ tetrahedral numbers, and the largest is $343867$.

theorem PollocksConjecture.pollock_tetrahedral.ncard_exceptions : IsGreatest NotSumOfFourTetrahedral 343867 ↔ NotSumOfFourTetrahedral.ncard = 241

As stated on Wikipedia/OEIS (A797), the set of exceptions has cardinality $241$.