---

Claim. Linmiao Xu's Lean 4 development Erdős #1139: large gaps between almost-primes, in the folder erdos-1139 of the public repository linrock/math-proofs (MIT license at the commit linked above, of 5 October 2026), proves the affirmative answer to Problem 1139 from one published theorem that it takes as a hypothesis. Its theorem Erdos1139.Palomar.erdos_1139_of_gtz derives

$$\limsup_{k\to\infty}\frac{u_{k+1}-u_k}{\log k}=\infty$$

from the proposition HasFixedSignedMixedPublishedVonMangoldtAsymptotics, the Green--Tao linear-forms asymptotic for the fixed systems the proof uses, as the paragraph on the hypothesis below explains. The route goes through double covers: if residue classes modulo primes $p$ or prime squares $p^2$ cover every $h\in[1,y]$ at least twice, the Chinese remainder theorem gives $N\in(Q,2Q]$, $Q$ the product of the moduli, with $\Omega(N+h)\ge3$ for $1\le h\le y$ (cover_crt_interval), and covers with $\log Q\le\varepsilon y$ for every $\varepsilon>0$ give the infinite limsup (limsup_top_of_sparse). The development takes the class $0$ modulo $p^2$ for the primes $p\le z$ and modulo $p$ for $z<p\le y/z$, after which the only targets with fewer than two hits are $1$, the primes, the semiprimes $pq$ with $p<z$ and $q>y/z$, and the prime powers $p^e$ with $z<p\le y/z$ (core_classification); it covers these with typed prime patterns in dyadic prime shells, counted by the hypothesis, and lets $z\to\infty$. Without the hypothesis it proves, by omitting a positive proportion of unused reserve primes from the double covering of Problem 689, that the limsup is at least some $A>1$ (limsup_strictly_gt_one) and that below every large $X$ some interval of length at least $c\log X$, for one fixed $c>1$, consists of integers with $\Omega\ge3$ (uniform_maximal_gap). It also proves that its hypothesis implies arbitrarily long arithmetic progressions of primes (prime_ap_of_gtz). The development's metadata describes it as AI-assisted, and names the candidate proof posted in the erdosproblems.com thread on 19 June 2026 (Price's claim page) as an earlier proposal of the squared-prime core, the typed prime patterns and the linear-forms route, while recording its own result as an independent proof.

Submission note. The Palomar registry's description of entry PALOMAR-2026-10-06-000001:

A Lean 4 formalization of unconditional bounds and conditional reductions for Erdős problem 1139 on consecutive P_2 almost-primes (Ω(u_k) ≤ 2). Extending Chojecki's (2026) Erdős 689 double-covering construction via protected-reserve omission, it proves unconditionally that limsup (u_{k+1} - u_k) / log(k + 1) ≥ A > 1 and that every large height X contains an almost-prime-free interval of length ≥ c log X (c > 1), alongside the mixed prime/prime-square CRT bridge, PNT primorial asymptotics, and squared-core deficiency classification. Using a squared-prime core and scale-adaptive dyadic prime shells, it also derives the full infinite-limsup conjecture conditionally from the Green–Tao–Ziegler (2010–2012) linear-forms asymptotic and proves its reverse implication to arbitrary-length prime progressions.

The formal statement. Statement.lean records the formal-conjectures declaration Erdos1139.erdos_1139 (FormalConjectures/ErdosProblems/1139.lean at the formal-conjectures commit of 2026-09-18) with the answer True: with $u$ the increasing enumeration, from index $0$, of the $n>0$ with $\Omega(n)\le2$, the limsup in the extended reals of $(u(k+1)-u(k))/\log(k+1)$ is $+\infty$. Since $u(k)$ is the problem's $u_{k+1}$, the ratio at $k$ is the problem's ratio at index $k+1$, so this is the problem's statement in the reading of its Formulation (prime factors counted with multiplicity, $1$ included), with the same polarity. AxiomAudit.lean proves that erdos_1139_of_gtz yields this proposition.

The hypothesis. HasFixedSignedMixedPublishedVonMangoldtAsymptotics (Proofs/AdaptiveMixedPublishedGTZCapstone1139.lean) has three fields, for three kinds of fixed system of integral linear forms: one prime pattern, the label form $P$ and target forms $A_dP+B_dC$ in two variables; two patterns sharing the label, in three variables; and two patterns of the same type sharing one target value, parametrized by three integer coordinates. For each fixed system and each fixed bounded open convex set $K$ inside the region where the forms are positive, a field asserts that the sum over the integer points $n$ of $NK$ of $\prod_i\Lambda(\psi_i(n))$, divided by $N^d$, tends as $N\to\infty$ to the volume of $K$ times a product over primes $\ell$ of local densities, with a Jacobian factor for the shared-target parametrization. For one pattern the density at $\ell$ is the proportion of $(\mathbb Z/\ell)^2$ on which no form vanishes, times $(\ell/(\ell-1))^t$ for $t$ forms. The development proves that the forms of each system are pairwise non-proportional, so each system has finite complexity. Each field is then a case of the asymptotic (1.7) of Green and Tao's generalized Hardy--Littlewood conjecture (Conjecture 1.2 of Linear equations in primes), which their Main Theorem proves for every system of finite complexity assuming the conjectures GI(s) and MN(s), both since proved (cited under Depends on below). The hypothesis asks for no uniformity: each field is one limit for one fixed system, and the kernel-checked deduction uses nothing more. So the hypothesis is a published theorem taken as a premise, not an unproven conjecture, and the claim is scoped full. This was checked here by reading the definitions: the one-pattern lattice is the set of integer points of $NK$, the positivity of the forms follows from the region, and its local density is Green and Tao's factor $\beta_p$. The two paired systems were compared with Green and Tao's statement. The development proves in Lean that each of their local factors is Green and Tao's $\beta_\ell$ for the system and equals the product of the one-pattern factors (AdaptiveSharedLabelFactorization1139 and AdaptiveSharedTargetActualFactorization1139). The shared-target sum runs over a lattice of rank $3$ in $\mathbb Z^4$, which SharedTargetFiberCovolume1139 parametrizes bijectively by $\mathbb Z^3$; the Jacobian factor of that field is the change of variables of this parametrization, which is not a Lean theorem and was checked by hand. Green and Tao's closed convex body against the hypothesis's open one, and the bounded box containing it, change only the error term. These readings are the corpus's own and are not an independent review.

Depends on. [[problems/integer_sequences/E0689/claims/2026_04_30_chojecki|Chojecki's claim on Problem 689]], whose double-covering construction, in Xu's own Lean formalization of it, the development extends for its unconditional bounds; no other wiki page. The hypothesis is the Main Theorem of B. Green and T. Tao, Linear equations in primes, Ann. of Math. 171 (2010), 1753--1850 (arXiv:math/0606088v2, with Conjecture 1.2), unconditional since B. Green and T. Tao, The Möbius function is strongly orthogonal to nilsequences, Ann. of Math. 175 (2012), 541--566, which proves MN(s), and B. Green, T. Tao and T. Ziegler, An inverse theorem for the Gowers $U^{s+1}[N]$-norm, Ann. of Math. 176 (2012), 1231--1372, which proves GI(s); none of them is formalized in Lean, and the library holds no card for them. The development also adapts third-party Lean modules, each at a pinned commit and listed with its license in its THIRD_PARTY.md: 25 Apache-2.0 modules of the PrimeNumberTheoremAnd project (the prime number theorem and Mertens estimates), with the nine Apache-2.0 modules of LeanArchitect that supply their blueprint attributes; two MIT-licensed modules of Will Blair's repository lean-proofs from its development for Problem 730 (the prime number theorem in a fixed arithmetic progression, derived from PrimeNumberTheoremAnd, and the statement of Mertens's reciprocal-prime asymptotic); and five Apache-2.0 modules of the Principia Math development for Problem 1054 (circle-method and Siegel--Walfisz inputs).

Formalization. The registry replays a submitted proof in Lean kernels and compares it with a challenge statement. Its entry, registered 2026-10-06T00:37Z, records Lean v4.35.0-rc2, the Mathlib revision the development pins, the permitted axioms propext, Quot.sound and Classical.choice, checks by the kernels nanoda and con-ron, and a 192-line challenge file importing only Mathlib that states the seven unconditional theorems. The challenge file does not state erdos_1139_of_gtz, so the registry compared neither the full statement nor its hypothesis with a challenge, and the axiom audit of that theorem is the development's own (AxiomAudit.lean). An automated review by GPT-6 Sol through Codex had a neutral outcome and no warnings. This corpus has neither built nor audited the development, so it gives no formalized evidence.

Standing. Claimed. No refereed publication or independent review is recorded, and a registry entry is not peer review. Bloom's catalog labeled the problem OPEN (page last edited 23 January 2026), and the development has no entry on the erdosproblems.com proof-claims tab, which was frozen on 6 October 2026.