---

Claim. For $k=3$ the answer to Problem 727 is yes: there are infinitely many $n$ with $(n+3)!^2\mid(2n)!$. Since $(n+2)!^2$ divides $(n+3)!^2$, the same $n$ give the case $k=2$, which the problem's source noted was unproved even for $k=2$. The manuscript, Johan Land, A carry-counting approach to the k = 3 case of Erdős Problem 727, dated 6 September 2026 and linked above in the repository at a pinned commit, takes $n=210t^2+391t+179$, for which each of $n+1$, $n+2$ and $n+3$ splits as a product of two linear forms in $t$. Restricting $t$ to a fixed arithmetic progression disposes of the small primes; for the remaining primes the divisibility is read through Kummer's carry count, controlled by uniform estimates for quadratic exponential sums and a finite residue computation. The only analytic input from outside the manuscript is the prime number theorem in fixed arithmetic progressions. The paper condenses an earlier manuscript kept in the repository's expert_advice/ folder.

Submission note. Posted to erdosproblems.com as a proof claim by Johan Land (account JohanLand) on 7 September 2026, giving "GPT-6-Astra, Fable 5.1, Gemini-3.8-Flash" as the AI used:

I have a candidate PARTIAL unconditional proof for k=3 (which would also establish k=2). The construction 𝑛 =210⁢𝑡2 +391⁢𝑡 +179 makes each of 𝑛 +1,𝑛 +2,𝑛 +3 a product of two linear forms. A fixed progression handles small primes, while carry counting, uniform quadratic exponential-sum estimates, and a finite residue calculation control the remaining failures. The only external analytic input is the classical prime number theorem in fixed arithmetic progressions. Formalized in lean.

Posted to the site's forum by Johan Land on 7 September 2026:

Thank you for this observation. I have a candidate unconditional proof for $k=3$, hence also $k=2$, using a different approach. The family $n=210t^2+391t+179$ makes each of $n+1,n+2,n+3$ factor into two linear forms; the argument exploits this structure through direct carry counting rather than Elliott–Chowla estimates.

The manuscript and lean formalization: https://github.com/beetree/math_erdos_727

Formal verification by the author. The repository, linked above at the same commit, holds a Lean 4 development whose terminal theorems Erdos727.erdos727_k3 and Erdos727.erdos727_k2 prove the right-hand sides of the formal-conjectures statements erdos_727 (at $k=3$) and its $k=2$ variant, compared against a pinned revision of that statement file by a script in the repository. The author's build audit reports the axioms propext, Classical.choice and Quot.sound only, with no sorry, project axiom or native_decide; the Mertens theorems it uses are vendored as proved Lean code. This corpus has not built or audited the development, so no formalized evidence is listed.

Covers. The cases $k=2$ and $k=3$. Every $k\ge4$ remains open.

Depends on. No page of this wiki.

Claimant and systems. Johan Land posted the result, with the repository link, to the problem's discussion thread on 2026-09-07 and submitted it to the proof-claims tab ten minutes later as a candidate partial proof; both postings are linked above. The tab names GPT-6-Astra, Fable 5.1 and Gemini-3.8-Flash as the systems used.

Standing. Pending. The site's label is open and its page does not mention the claim; the proof-claims entry carries no comments, no publication exists, and this corpus has checked neither the manuscript nor the Lean development.