---

Claim. For $k=12$, $k=13$ and $k=16$ there is an $n$ with $\prod_{0\le i\le k}(n-i)\mid\binom{2n}{n}$, as Problem 396 asks: the least such $n$ are

$$5048891644646,\quad 18253129921842,\quad 20021368432952099 .$$

They are the terms $a(12)$, $a(13)$ and $a(16)$ of the OEIS entry A375077, whose extension lines credit them to Justin Dehorty on 23 March 2026 and 28 July 2026. Dehorty's thread post of 23 March 2026 reports an exhaustive search in their repository jdehorty/erdos396 (linked at its commit of 4 April 2026) that found the witnesses for $k=8$ to $k=13$ and certifies each as minimal: every smaller integer is ruled out. The search runs over consecutive members of the set of $n$ with $n\mid\binom{2n}{n}$, and its completeness rests on the post's Small Prime Barrier Theorem, that a witness with a factor $n-i$ outside that set fails only at a prime $p<2k+1$; the repository's formal/ folder proves that theorem and its tightness in Lean 4 with Mathlib. The Lean proof covers the barrier theorem, not the search, and this corpus has not built it. The post names the AI systems used: GPT-5.4 Pro (extended thinking) and Google Gemini 3.1 DeepThink for proof exploration and adversarial review, and Claude Opus 4.6 for coding the Rust search pipeline and the Lean formalization. The post dates Dehorty's own finds of $a(8)$ and $a(10)$ to January 2025 and of $a(11)$ to $a(13)$ to February 2026; the entry credits $a(8)$ to $a(11)$ to Kesarwani, whose page is Kesarwani 2026, and this page follows the entry. A witness is checked through Kummer's theorem, as Stephan's page explains; the problem asks for existence, so minimality is context.

Submission note. Posted to the site's forum by Justin Dehorty on 23 March 2026:

$\largeExtending OEIS A375077 through k=13$

$Exhaustive search, validation, and a formally verified barrier theorem$

Over the past several months I have been running an exhaustive computational search for [396] witnesses, extending OEIS A375077 with 6 new terms at the initial time of discovery (2 new terms at the time of this post). The full codebase, validation certificates, and a machine-checked proof are publicly available at github.com/jdehorty/erdos396.

New values:

$\begin{array}{c|c|c|c} k & a(k) & \text{Search range} & \text{Date found*} \ \hline 8 & 339{,}949{,}252 & 0\text{–}340\text{M} & \text{2025-01-17} \ 9 & 1{,}019{,}547{,}844 & 0\text{–}17.6\text{B} & \text{2026-03-16 (corrected)} \ 10 & 17{,}609{,}764{,}994 & 0\text{–}17.6\text{B} & \text{2025-01-20} \ 11 & 1{,}070{,}858{,}041{,}585 & 0\text{–}2\text{T} & \text{2026-02-09} \ 12 & 5{,}048{,}891{,}644{,}646 & 0\text{–}6.15\text{T} & \text{2026-02-11} \ 13 & 18{,}253{,}129{,}921{,}842 & 0\text{–}25\text{T} & \text{2026-02-16} \end{array}$

*Note: Dates reflect my own personal records of when each value was first found, not when results were submitted or published. The jumps in pace (particularly from k=11 onward) correspond to successive sieve improvements: the v1 prefilter (7x), the fused sieve pass (15x), and finally Kummer-based valuation for all primes (31x single-threaded throughput).

Each value has a computational certificate of minimality: every integer below the claimed witness has been checked and ruled out.

Note on $k=9$: the original governor-run search found a witness at $17{,}609{,}764{,}993$. A subsequent full validation pass (checking every integer, not just governor-run candidates) found the true minimum at $1{,}019{,}547{,}844$.

$Method.$ The search is built around the Governor Set $G = {n : n \mid \binom{2n}{n}}$ (OEIS A014847, density $\approx 12.3\%$ by Ford-Konyagin). All known witnesses have every block term $n, n-1, \ldots, n-k$ in $G$. A fused segmented sieve strips small prime factors and checks the Kummer carry condition $\nu_p(n) \leq \nu_p\!\binom{2n}{n}$ inline, rejecting ${\sim}87\%$ of integers in a single pass. The $\sqrt{2n}$ large-prime-factor barrier provides additional fast rejection. Runs of $k+1$ consecutive governors are candidate witnesses, each verified by the full inequality $\sum_{i=0}^{k} \nu_p(n-i) \leq \nu_p!\binom{2n}{n}$ at every prime $p$.

$The Small Prime Barrier Theorem.$ The governor-run search cannot detect witnesses where some block term fails to be a governor. I proved that any such non-governor failure must occur at a prime $p < 2k+1$. For $k=13$ this is just 9 primes: $\{2,3,5,7,11,13,17,19,23\}$. The proof uses Kummer's theorem and a carry invariance lemma for base-$p$ self-addition; the bound $2k+1$ is tight (via Bertrand's postulate). The Small Prime Barrier Theorem and its tightness are formally verified in Lean 4 + Mathlib (no sorry/admit); the formal proof covers the carry invariance lemma, the barrier theorem itself, and the tightness result via Bertrand's postulate - not the computational search.

This yields a provably complete validation method: screen every integer at the barrier primes, then fully verify survivors. The validate binary implements this for $k=8$ through $k=13$, producing minimality certificates independent of the Governor Set Completeness Conjecture.

$Verification.$ The repository includes: (1) a Rust verifier and a stdlib-only Python verifier for witness validity; (2) the Lean 4 formal proof of the Small Prime Barrier Theorem (justifying the completeness of the validation algorithm); (3) published validation certificates with coverage invariants and build metadata tied to specific source revisions; (4) an independent report checker that recomputes invariants from the JSON reports. Full details at github.com/jdehorty/erdos396.

Note: AI usage comprised GPT-5.4 Pro (extended thinking) and Google Gemini 3.1 DeepThink for proof exploration and adversarial review, and Claude Opus 4.6 for coding the Rust-based search pipeline and Lean 4 formalization. The Lean 4 formal proof is machine-checked (no sorry/admit), and all computational claims are backed by deterministic validation certificates; see docs/trust.md in the repository.

Covers. The instances $k=12$, $k=13$ and $k=16$ of the question, each with the answer yes by an explicit witness. The $k=14$ term, credited jointly, is on its own page.

Depends on. No page of this wiki.

Standing. The entry is an edited database record and the thread post an unrefereed announcement; the site's commentary on a problem it labels OPEN points to the entry without accepting a result. The claim stays claimed.