Claims

../

2025_08_28_cambie_kovac_tao: For n a suitable power of two, every binomial coefficient in row n is divisible by the r-th power of 2 or of a chosen prime, so S(n) is unbounded; worked out in the site's discussion thread and formalized in Lean by Tao.

2025_12_21_yuan: A Lean 4 proof, produced by Seed-Prover 1.5 and posted by Zheng Yuan on 21 December 2025, that S(n) is unbounded, by a construction different from Cambie, Kovač and Tao's; a version of its Lean code was built here.

---