---

Claim. The answer to Problem 379 is yes: $\limsup_{n\to\infty}S(n)=\infty$, where $S(n)$ is the largest $s$ such that every $\binom{n}{k}$ with $1\le k<n$ is divisible by $p^s$ for some prime $p$ depending on $k$. The result is proved in Lean 4 as the theorem erdos_379 of the code that Zheng Yuan linked from the problem's discussion thread on 21 December 2025, presenting it as the proof found by Seed-Prover 1.5, an automated theorem-proving system; the claimant is the submitter, Yuan. The construction differs from the one of Cambie, Kovač and Tao on their claim page: for $M\ge1$ and $R=2^{M-1}$ it takes a prime $q>R$ dividing $2^{2\cdot R!}+1$ and an exponent $L$ with $2^L\equiv-1\pmod{q^M}$, and considers the row $n=R\cdot2^L=2^{M+L-1}$: an entry $\binom nk$ with $2^L\nmid k$ is divisible by $2^M$, by the $2$-adic valuation of a binomial coefficient in a power-of-two row, and an entry with $k=j\cdot2^L$, $1\le j<R$, is divisible by $q^M$, by Kummer's theorem, since the congruence $2^L\equiv-1\pmod{q^M}$ forces a carry in each of the lowest $M$ base-$q$ digits when $k$ is added to $n-k$. Taking $M\to\infty$ gives $S(n)\ge M$ along a sequence of rows. A version of the code is the file Erdos379.lean in Boris Alexeev's lean-proofs collection (the second link, pinned), whose header declares it a Lean formalization of a solution to the problem with Cambie, Kovač and Tao as informal authors and Seed-Prover 1.5 and Zheng Yuan as formal authors and points to the thread post.

Submission note. Posted to the site's forum by Zheng Yuan on 21 December 2025:

Check the proof from Seed-Prover 1.5.

Depends on. No page of this wiki.

Acceptance. Formalized. This corpus's verification built Alexeev's lean-proofs collection at the pinned commit of 2026-09-15 (Lean v4.33.0, Mathlib v4.33.0, the toolchain of its src/latest folder, in which the module builds), compiling the module ErdosProblems.Erdos379 and the collection's comparator challenge for the problem, and checked the axioms of Erdos379.erdos_379, which are exactly propext, Classical.choice and Quot.sound; the module contains no sorry. The challenge ComparatorChallenges/ErdosProblems/Erdos379.lean pins that theorem together with the definition Erdos379.S, and the fingerprint of both was found identical to the challenge. What was built is the collection's file, a version of the code posted in the thread; the code as posted was not itself built. The statement was audited clause by clause against the problem's Statement and is exact: S n is the supremum of the exponents $s$ such that every $\binom nk$ with $1\le k<n$ is divisible by $p^s$ for some prime $p$; for $n\ge2$ this set contains $0$, is closed downward and is bounded, since $p^s\le\binom n1=n$, so S n is the problem's $S(n)$, and the junk values $S(0)=S(1)=0$ cannot affect a limsup; the theorem says that the limsup of S n in the extended natural numbers is $\top$, which for a sequence of finite values holds exactly when $S$ is unbounded, the question asked. The definition and the theorem are verbatim the challenge's, the formal-conjectures statement file states the same theorem, and the file's lemmas follow the construction above. Not reviewed: the site's label PROVED (LEAN) and its remarks credit the proof of Cambie, Kovač and Tao and Tao's formalization and do not mention this proof, and no outside reviewer has published an examination of it. Not refereed: there is no journal publication; the result exists as the thread post and the Lean code.