---

Claim. Write $P^+(n)$ for the largest prime factor of $n$ and $\rho$ for Dickman's function. For every fixed $a,b\in(0,1)$,

$$\lim_{X\to\infty}\frac1X\,\#\{2\le n\le X:\ P^+(n)\le n^{a},\ P^+(n+1)\le n^{b}\}=\rho(1/a)\,\rho(1/b),$$

the limit over all real $X$ with ordinary counting (Theorem 1.1 of the release's manuscript The joint Dickman law for consecutive integers, 2026-09-24, filed as the library's intake card). So the density asked for by Problem 928 exists and equals the product of the two Dickman densities: the events $P(n)<n^{\alpha}$ and $P(n+1)<(n+1)^{\beta}$ are independent in the sense Erdős asked for, which the manuscript calls the Erdős–Pomerance joint Dickman conjecture. Its Section 11 also gives the law with the fixed thresholds $X^{a}$ and $X^{b}$ and the upper-tail independence that Erdős and Pomerance conjectured. Its Corollary 1.2, that $P^+(n)<P^+(n+1)$ has natural density $1/2$, follows because the continuous limiting law gives the diagonal no mass; it is the question of Problem 371, which carries its own account. The method replaces the largest prime factor by finitely many counts of prime factors in bins $(x^{k/J},x^{(k+1)/J}]$, so that the joint law becomes a mixed decorrelation $\frac1x\sum_{n<x}g_x(n)F_x(n+1)\to0$ between two bin characters with different phase vectors, one centered; the decorrelation is proved through an amplification of the correlation over an auxiliary logarithmic scale, an independent-site kernel, a second moment for the latent rows, smoothing on logarithmic and residue space, and the vanishing of the main energy.

Bridge to the statement. The problem's set uses strict inequalities and the threshold $(n+1)^{\beta}$ for $n+1$; the manuscript and the Lean use $\le$ and $n^{b}$. Up to $X$ the two sets differ by at most $\pi(X^{\alpha})+\pi((X+1)^{\beta})$ integers: an $n$ in one set and not the other either has $P(n)=n^{\alpha}$ exactly, so that $n=p^{1/\alpha}$ for a prime $p\le X^{\alpha}$, or has $P(n+1)$ equal to a prime $q$ with $n^{\beta}<q<(n+1)^{\beta}$, an interval of length below $1$ that determines $n$ from $q\le(X+1)^{\beta}$. Both counts are $o(X)$, so the densities of the two sets agree. The bridge is elementary and is stated here, not in Lean.

Depends on. No page of this wiki.

Acceptance. Formalized. The release's lean/ folder states the theorem as OAI.JointDickmanPaper.joint_law in the comparator challenge JointDickman.lean (the third link), with the ordering corollaries increasing_order and decreasing_order, proved in its solution module OAI.NumberTheory.JointDickman.PaperMain (in the tree of the second link): the predicate uses Mathlib's Nat.maxPrimeFac, the density counts $2\le n\le\lfloor X\rfloor$ and divides by the real $X$, and the Dickman function is defined through its delay equation; the challenge's configuration permits only propext, Quot.sound and Classical.choice. This corpus's verification built OAI.JointDickmanPaper.joint_law at the pinned revision of 6 October 2026 with the toolchain leanprover/lean4:v4.34.1 and checked its axioms, which are exactly those three, with no sorry; its fingerprint was found identical to the challenge. The statement audit found the declaration exactly Theorem 1.1 as displayed above, for every real $a,b\in(0,1)$, a hypothesis that can be met: Nat.maxPrimeFac is the true largest prime factor for every $n\ge2$, and the count uses only $n\ge2$; realDensity is the ordinary two-sided natural density over real $X$, which leaving out $n=0,1$ does not change; and the formal $\rho$, built level by level from the value $1$ on $[0,1]$ and the equation $\rho(u)=1-\int_1^u\rho(t-1)\,dt/t$ through continuous approximants, so that its integrals are genuine and not junk values, is the Dickman function, evaluated at $1/a>1$ and $1/b>1$. The audit also checked the bridge above, which is correct and is stated on this page, not in Lean; since the Statement asks only whether the density exists, the theorem with the bridge settles it in full. Not reviewed or refereed: no outside review, referee report or acceptance by the site is known (the site labels the problem OPEN, its page last edited 3 April 2026), and no review of the manuscript's proof is recorded. The manuscript places the result against the earlier literature: Teräväinen 2018 proved the product law in logarithmic density (Theorem 1.14 there) and the ordering in logarithmic density $1/2$; Wang [Wa21] proved the natural density under the Elliott–Halberstam conjecture for friable integers, the accepted conditional claim on Wang 2021; Tao and Teräväinen obtained the ordinary law outside an exceptional set of scales; and the lower natural density of each ordering rose from Erdős and Pomerance's $0.0099$ through the $0.2017$ of Lü and Wang to $0.280$ in Yang's 2026 preprint (arXiv:2607.16032), none asserting that the density exists. The release's README states that its manuscripts and supporting proof artifacts were produced by an internal OpenAI model and that the collection includes results at different stages of verification; the manuscript's author line is OpenAI and names no person.