---

Claim. Srihari Mysore's draft note Binomial coefficients $\binom n2$ that are products of consecutive primes, dated 30 September 2026 and linked with its code from a post in the site's discussion thread that day, treats the case $k=2$ of Problem 386, whose known solutions are $n=4,6,15,21,715$. Its Lemma 2 is a balance inequality: if every prime factor of $\binom n2$ lies in $[p,r]$ with $p\ge5$ and $\binom n2$ has $k$ prime factors counted with multiplicity, then $(r/p)^{\lfloor k/2\rfloor}\ge2-1/p$, because $n$ and $n-1$ split the primes into two products in ratio almost exactly $2$; this is an explicit form of a thread observation of 24 August 2025 that each fixed block length allows only finitely many solutions. With Dusart's explicit prime-gap estimates (a 2010 preprint, and Ramanujan J. 45 (2018), Corollary 5.5) and computer searches, its Theorem 9 shows that any further solution is a product of at least $137$ consecutive primes, and of at least $1924$ with the 2018 estimate; its Theorem 8 finds no further solution with $n\le10^{12}$ by computation alone, none with $n\le10^{682}$ with the 2010 estimate and none with $n\le10^{9614}$ with the 2018 estimate; and its Theorem 10 excludes every block that starts below $100$ and ends at a prime at most $4\cdot10^9$, so the primorial equations $n(n-1)=r\#$ and $n(n-1)=2\cdot r\#$ have no new solution with $r\le4\cdot10^9$. The computations are ordinary C and Python programs, cross-checked against each other but not formally verified. The repository's Lean 4 code proves the arithmetic core of the balance inequality without Mathlib, its block form against the objects of the formal-conjectures statement with Mathlib, and the lemma that $\binom n2$ is not prime for $n\ge4$; the prime-gap theorems and the computations are not formalized. The post says the Lean proofs were generated with AI, and the note's acknowledgements say that the computations, proofs and formalization were developed with substantial assistance from Claude (Anthropic), an AI model. The author says the note does not solve the problem.

Covers. For $k=2$, the solutions that are products of at most $1923$ consecutive primes: they are exactly $n=4,6,15,21,715$, a partial no for each of those block lengths. The searches below a bound on $n$ exclude no infinite family and are not covered.

Depends on. No page of this wiki.

Standing. The note is an unrefereed draft, no outside reviewer has recorded accepting it, and the site labels the problem OPEN without mentioning it, so the claim is claimed. The Lean code is third-party, not built here, and does not state these theorems, so no formalized evidence is listed.