Wikipedia · textbook · AMS 11
mediumknown result, no worker yet
Pollock's (tetrahedral numbers) conjecture
Theorem · pollock_tetrahedral.ncard_exceptions
As stated on Wikipedia/OEIS (A797), the set of exceptions has cardinality .
Formal statement · Lean 4.lean
theorem pollock_tetrahedral.ncard_exceptions :
type_of% pollock_tetrahedral.salzer_levine ↔
NotSumOfFourTetrahedral.ncard = 241 := by
sorryProof. sorry
Nobody has tried yet.