---

Claim. Let $P(n)$ be the largest prime factor of $n$, with $P(1)=1$, and let $\rho$ be the Dickman function. Theorem 1.1 of the release's manuscript The joint Dickman law for consecutive integers (2026-09-24) states that 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 unweighted counting: the two normalized largest prime factors $\log P(n)/\log n$ and $\log P(n+1)/\log n$ have independent limit laws in natural density. Its Corollary 1.2 is the statement of Problem 371: the set of $n$ with $P(n)<P(n+1)$ has natural density $1/2$, and so has the set with the reverse strict inequality. The deduction is the manuscript's own: the common marginal law is continuous, so the product law gives the diagonal no mass, and the two strict orderings have equal density by symmetry. The same theorem answers Problem 928, whose page carries the family's claim on that question. The release's account of the method: the largest prime factor is replaced by finitely many prime counts in bins $(x^{k/J},x^{(k+1)/J}]$, and the joint law is reduced by finite Fourier inversion to the decorrelation of two bin characters at the shift one. The manuscript places the result against the literature the page cites: positive lower density for each ordering by Erdős and Pomerance (Erdős and Pomerance 1978), lower density at least $0.2017$ by Lü and Wang (Lü and Wang 2025), logarithmic density $1/2$ by Teräväinen (Teräväinen 2018), density $1/2$ at almost all scales by Tao and Teräväinen (Tao and Teräväinen 2019), and the natural density under the Elliott–Halberstam conjecture for friable integers by Wang. The intake card openai_2026_joint_dickman_law_consecutive_integers digests the manuscript.

Formalization. The release's lean/OAI/NumberTheory/JointDickman/ folder at the pinned revision proves the corollary as OAI.JointDickmanPaper.increasing_order, pinned by the comparator challenge ComparatorChallenges/JointDickman.lean, whose theorems are statements only: realDensity P X is the number of $n$ with $2\le n\le\lfloor X\rfloor$ satisfying P, divided by the real $X$, and the declaration asserts that realDensity (fun n => n.maxPrimeFac < (n + 1).maxPrimeFac) tends to $1/2$ as the real $X$ tends to infinity, where Nat.maxPrimeFac is Mathlib's largest prime factor. The same challenge pins joint_law, the theorem with both thresholds based at $n$, and decreasing_order, the reverse ordering. The corpus's source-level audit compared the declaration with the problem's Statement clause by clause (the function, the strict inequality and its direction, and natural density as a two-sided limit over real $X$, which omitting $n=0,1$ does not change) and judged it exact; it also found that the formal-conjectures statement erdos_371 has the same predicate and the same notion of density.

Depends on. No page of this wiki; the manuscript cites published analytic inputs, among them the theorems of Matomäki and Radziwiłł, of Matomäki, Radziwiłł and Tao, and the Selberg–Delange method.

Acceptance. Formalized. This corpus's verification built OAI.JointDickmanPaper.increasing_order at the pinned revision of 6 October 2026 with the toolchain leanprover/lean4:v4.34.1 and checked its axioms, which are exactly propext, Classical.choice and Quot.sound, with no sorry; the comparator challenge lean/ComparatorChallenges/JointDickman.lean pins the declaration, and its fingerprint was found identical to the challenge. The statement audit found the declaration an exact statement of the problem: the predicate is the strict inequality n.maxPrimeFac < (n + 1).maxPrimeFac, in the direction the Statement asks for; Nat.maxPrimeFac is the true largest prime factor for every $n\ge2$, and the excluded $n=1$ does not change the density; realDensity is the ordinary natural density, a two-sided limit over real $X$, not a logarithmic density, a density along a subsequence or a lower density; and the target $1/2$ is the real number, not the natural-number quotient $0$. The same build covers OAI.JointDickmanPaper.decreasing_order, with the same axioms and fingerprint match, which proves this page's secondary sentence that the reverse strict ordering also has density $1/2$; on its own it does not give the problem's statement, which would also need the diagonal $P(n)=P(n+1)$ to have density $0$, so the full scope rests on increasing_order. Not reviewed or refereed: no outside review, referee report or acceptance by the site is recorded, and the site's page, last edited 23 January 2026, labels the problem OPEN and does not mention the release. 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.