---

Claim. For $k\ge2$ let $g(k)$ be the least $n>k+1$ such that no prime $p\le k$ divides $\binom nk$, and write $L_k=\operatorname{lcm}(1,\ldots,k)$. Ethan Yang's manuscript "A least-common-multiple bound for the Erdős–Selfridge function" (dated 26 September 2026, 8 pages) proves, as its Theorem 1.1, that there is an integer $K\ge2$ such that for every $k\ge K$ some integer $n$ satisfies

$$k+1<n<L_k \qquad\text{and}\qquad p\nmid\binom nk\ \text{ for all primes }p\le k,$$

so that $g(k)<L_k$ for every sufficiently large $k$. This is the comparison Ecklund, Erdős and Selfridge asked for at the end of their paper Ecklund, Erdős and Selfridge (1974), which the site's remarks record as their conjecture; their own upper bound $g(k)\le\exp((1+o(1))k)$ does not decide it, since $\log L_k\sim k$. The manuscript fixes no numerical value of $K$.

Submission note. Posted to erdosproblems.com as a proof claim by Ethan Yang (account EthanYang) on 26 September 2026, giving "GPT-6 Astra, GPT-5.6 Sol" as the AI used:

I give a complete proof of the eventual least-common-multiple conjecture of Ecklund, Erdős, and Selfridge: for every sufficiently large integer k, g(k) < L_k = lcm(1,...,k). The proof constructs n = Mt-1 with k+1 < n < L_k. The modulus M modifies L_k by adding small-prime factors and removing primes near k. Lucas's theorem handles the small primes automatically and converts the remaining conditions into forbidden residue classes for t. The prime number theorem controls the size of M and the total forbidden density. Truncated inclusion-exclusion, with an explicit Chinese-remainder counting error, then produces a surviving multiplier in the required finite interval. Notes: GPT-6 Astra generated the mathematical proof and was used for statement reconstruction, review, and writing. GPT-5.6 Sol was used for the Lean implementation. The Lean 4 proof is complete and unconditional. All PNT results used are formally proved. The final theorem has no undischarged hypotheses or sorryAx; its axiom report contains exactly propext, Classical.choice, and Quot.sound. This claim settles the eventual lcm conjecture, not the sharp growth estimate or successive-ratio conjectures. No independent human expert review is claimed; I welcome checking of the statement correspondence and exposition.

Argument. The candidates are $n=Mt-1$ with $1\le t\le T=\lfloor e^{\varepsilon k/2}\rfloor$ and $\varepsilon=1/1000$, where the modulus $M$ is $L_k$ with every prime in $((1-\varepsilon)k,k]$ removed and one extra factor of each prime $p\le\varepsilon^2k$ added. The prime number theorem gives $\log(M/L_k)=(\varepsilon^2-\varepsilon)k+o(k)$, so every candidate lies strictly between $k+1$ and $L_k$ once $k$ is large. By Lucas's theorem the extra factor makes the low base-$p$ digits of $n$ equal to $p-1$, so no prime $p\le\varepsilon^2k$ divides $\binom nk$ whatever $t$ is; each larger prime $p\le k$ instead forbids a set of residues of $t$ modulo $p^2$, of density at most $k/p^2$ for the middle primes and about $(k-p)/p$ for the primes near $k$, so the total forbidden density is $O(\varepsilon^2k/\log k)$. An inclusion–exclusion truncated at an odd order $J=O(\varepsilon^2k/\log k)$, with an explicit bound of size $\exp(O(\varepsilon^2k))$ on the residue-class counting error from the Chinese remainder theorem, then shows that some $t\le T$ escapes every forbidden class, because the interval length $\exp(\varepsilon k/2)$ absorbs that error. The manuscript notes that the method balances these terms on an interval exponential in $k$ and does not place a witness on the conjectured scale $\exp(O(k/\log k))$.

Covers. The eventual strict upper bound $g(k)<L_k$, for all $k$ beyond an unspecified threshold. It does not estimate $g(k)$: it leaves the order of $\log g(k)$ open between Konyagin's lower bound $g(k)\ge\exp(c(\log k)^2)$ and the bound $\log L_k\sim k$, says nothing about the conjectured scale $\log g(k)\asymp k/\log k$, gives no numerical threshold, and does not touch the conjectures of Ecklund, Erdős and Selfridge on $\limsup g(k+1)/g(k)$ and $\liminf g(k+1)/g(k)$.

Claimant and systems. The manuscript's tool disclosure says that the mathematical proof was generated by GPT-6 Astra using Codex, that separate GPT-6 Astra sessions reviewed the argument and reconstructed the formal statement, that GPT-5.6 Sol implemented the Lean proof, and that GPT-6 Astra prepared the manuscript and its literature review; the author's contributions were problem selection, direction of these workflows, provision of literature and editorial decisions, and the author states not having supplied the argument or checked the proof by hand. The forum entry names the systems as GPT-6 Astra and GPT-5.6 Sol. The human submitter, Ethan Yang (University of Michigan), is the claimant. The manuscript is licensed CC BY 4.0 and the repository Apache 2.0.

Formalization. The repository linked above at its commit of 26 September 2026 holds a Lean 4.27.0 development on Mathlib (21 files, 4,195 lines by its README) whose final theorems are Erdos1095.erdos1095_target, an explicit witness $n$ with $k+1<n<L_k$ and no prime divisor $p\le k$ of $\binom nk$ for every $k$ beyond one threshold $K\ge2$, and Erdos1095.erdos1095_main, the inequality $g(k)<L_k$ for every $k\ge K$. The definition of $g$ is copied from the formal-conjectures file for this problem, at the commit the repository's correspondence table cites, as the infimum of $\{m: k+1<m,\ k<\operatorname{minFac}\binom mk\}$; that file defines $g$ but states no form of the lcm conjecture, so the proposition is the repository's own reconstruction, and its correspondence table records that the inequality is deduced from a constructed member of the defining set rather than from the value of an infimum, which Lean sets to $0$ on the empty set. The prime number theorem comes from the PrimeNumberTheoremAnd project at a pinned commit. The README reports an axiom surface of propext, Classical.choice and Quot.sound for the final theorem and no sorry in its dependency surface, while two unrelated declarations of the pinned PNT package carry sorry warnings. This corpus has not built or audited the development, so it is a formalization link and no formalized evidence.

Standing. Posted on the problem's proof-claims tab on 26 September 2026 as a partial claim, with the manuscript and the repository as its links. The site's label is OPEN and its page was last edited on 21 June 2026, so the curator has not credited the result. The one comment on the claim, of 2 October 2026, points to a record on the Significance site, which pins the manuscript and repository, lists review tasks, and records no independent Lean build, mathematical assessment or written review; it presents itself as a reading map, not a correctness verdict. The manuscript is not refereed and no one has recorded accepting it, so the claim is claimed.