---

Claim. With $P(n)$ the largest prime factor of $n$, an interval $[u,v]$ of positive integers bad when $P(\prod_{u\le m\le v}m)^2$ divides the product, and $B(x)$ the number of $n\le x$ covered by a bad interval,

$$B(x)\sim\#\{n\le x:P(n)^2\mid n\}\qquad(x\to\infty),$$

the question of Problem 380, answered yes with no error term. The claim is the theorem erdos380 : B ~[Filter.atTop] repeatedLargestPrimeCount of the development Erdos380.lean in the lean-proofs repository, committed by Boris Alexeev on 2026-08-26 (the formalization link, pinned to that commit); the file's docstring states the definitions: intervalPrime u v is the greatest prime factor of the whole product, a bad interval is positive and nonempty with product greater than one, witnessing endpoints may exceed the counting cutoff, and the convention largestPrimeFactor 1 = 1 puts $1$ into the comparison set, handled by a separate lemma. The development's route, as its docstring describes it: the proof counts the singleton anchors (the $n$ with $P(n)^2\mid n$) and shows that every further covered point contributes little-o of that count; explicit smooth-number bounds and prime compression replace a local smooth-number asymptotic; the neighbors of an anchor in a short interval are counted by their distance from it, giving a harmonic sum; the remaining intervals are controlled by one high-order smooth-run sieve and a large-square exclusion, without a prime-gap theorem or a subdivision by intermediate interval lengths. The modules AntiSieve.lean and CutoffSieve.lean formalize Lemma 2.7 and Corollaries 2.8 and 2.9 of Tao's preprint [Ta26c], the finite Fourier uncertainty estimate, and the short-interval modules (singleton anchors, prime boxes, smooth-shift divisibility mass and moments) follow the anti-sieve strategy of that preprint without naming it; the long-interval module says that no theorem on gaps between primes is required, where Tao's Theorem 1.7 rests on the Guth–Maynard zero-density estimate. The development therefore proves the asymptotic by a route of its own and does not declare itself a formalization of Tao's result, which is the accepted claim Tao 2026; it proves the qualitative statement only, without Tao's relative error $O((\log x)^{-1+o(1)})$.

Depends on. No page of this wiki.

Standing. The repository's note for the problem (the record link) says only that the file is a formalized proof of Problem 380 and names no author and no AI system; the file's header names neither. As of 2026-10-07 the site's page lists no formalised statement and its forum thread does not mention the development; formal-conjectures has no statement file for the problem, and the community database's commit of 2026-03-31 changed the problem's status to proved, and the database lists it as unformalized (as of 2026-10-06). This corpus has not built the development or audited its statement, and there is no publication or outside review, so the claim stays claimed. It does not change the problem's standing, which Tao's curator-accepted preprint settles.