Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Let be the set of squarefree such that
for every , where is the squarefree part
of , the product of the primes dividing to an odd power (the paper
writes it and, in its Section 7, calls it a kernel).
Theorem 1.1 of the paper: has a positive natural density
, the members of up to with a prime factor above
that lie in number , and so
the lower density of is at least . This answers
the example question of
Problem 374, the conjecture of
Erdős and Graham that ; the paper's own statement adds that it
neither asserts that has a natural density nor gives an effective value
of . The source is J. S. Hartley and M. A. Olson, A Resolution of
Erdos 374; by the paper's title footnote, the first version, containing
Theorem 1.1, was posted on SSRN on 2026-09-29. The revised paper is in the
paper/ folder of the repository linked above, first committed on 2026-10-04;
the page follows it at the pinned commit of 2026-10-06. The revised paper
extends the claim: its Theorem 7.1 adds, for every ,
with
over the distinct values
of the squarefree parts, and lower densities at least for and
for , so that and
for , the orders of growth the problem asks for. The forum claim of
2026-10-02, labeled partial, described only the positive lower density of
; the revised paper and the claimant's comment of 2026-10-05 assert the
whole determination, which is the claim this page records.
The argument runs as follows. Canceling squares turns a five-factorial product with into the condition that be a square, where , and , so every representation is governed by two blocks of consecutive integers (four factorials being the case ). The gcd conditions defining rule out exactly the paired representations with , and has a positive natural density because the squarefree integers failing the th condition are divisible by a divisor of above , so the proportion failing it is at most , since and , a bound summable in . The squarefree integers with no prime factor up to meet every condition with and have density , more than the removed by the conditions with once is large, and the densities for finitely many conditions converge uniformly to that of . For an endpoint with a prime factor above the remaining representations are handled in two steps: a lemma on the logarithmic mass of the primes dividing a long block exactly once, proved with the equidistribution theorem of Matomäki, Radziwiłł, Shao, Tao and Teräväinen for sums over primes of smooth functions of and , shows that the lower block cannot be much longer than the upper one, and the largest prime below , which Harman's almost-all theorem on primes in short intervals places within of for all but endpoints, forces the upper block to be that short; the surviving short-block representations are then counted by a sieve anchored at the large prime factor of , in which Weil's bound for quadratic character sums of polynomials and the analytic large sieve show that only endpoints admit one. The six-factorial identity of Erdős and Graham supplies a representation of length six for each of these , so for a proportion of the integers up to , the factor arising from the sum over the cofactors of the large prime factor .
Submission note. Posted to erdosproblems.com as a proof claim by Jusvin Dhillon, Jonathan S. Hartley, Matthew A. Olson (account jonhartley) on 2 October 2026, giving "ChatGPT Astra; Google’s Gemini 3.1 Pro and Gemini 3.8 Flash; Anthropic’s Claude Opus 5.5 and Claude Fable 5.1; xAI’s Grok 4.7" as the AI used:
Hartley, Olson, and Dhillon give a proof that has positive lower density, proving the Erdős–Graham conjecture . They construct a positive-density family of squarefree integers with a very large prime factor, excluding the principal paired representations. Other four- and five-factor representations reduce to two intervals of consecutive integers. A reciprocal-prime equidistribution theorem of Matomäki–Radziwiłł–Shao–Tao–Teräväinen, together with Harman's short-interval theorem, forces both intervals to be short for almost all endpoints. The large prime factor then anchors the remaining square condition; Weil's bound and the large sieve show that the exceptions are . The Erdős–Graham six-factor identity then gives for a positive proportion of integers. Posted to SSRN on 29 Sep 2026.
Authorship and the parallel proof. The forum claim of 2026-10-02 names three claimants, Dhillon, Hartley and Olson; the paper at the pinned commit lists Hartley and Olson, after a commit of 2026-10-06 that updated the author list, and this page follows the paper. The title footnote records that Yudin independently proved the positive lower density of , the bound and the asymptotic for , Yudin's preprint appearing on arXiv on 2026-10-01, two days after the SSRN posting, and lists the differences between the arguments: Huxley's short-interval theorem against Harman's almost-all theorem for the primes, a direct use of the equidistribution estimate for both block lengths against the valuation-one prime-mass lemma (Lemma 4.1) combined with the short-gap corollary drawn from Harman's theorem (Corollary 6.2), a different arithmetic set of endpoints, and Tao's uniform Pell bound against an elementary count for .
Standing. The claim is pending. The site's proof-claims tab lists it as a
partial proof claim, matching that submission; the revised paper and the
claimant's comment of 2026-10-05 on the claim, which calls the repository a
full Lean verification of the problem, assert the whole determination. The
site's label is unchanged and the curator has not credited the result, so
there is no acceptance evidence. The paper's acknowledgment says it was
prepared with AI assistance in derivation, internal checking, source
verification, exposition and formalization, naming ChatGPT Astra, Google's
Gemini 3.1 Pro and Gemini 3.8 Flash, Anthropic's Claude Opus 5.5 and Claude
Fable 5.1, and xAI's Grok 4.7, the systems the claim's tools field also names.
The repository's README (Lean v4.35.0-rc2 on a pinned Mathlib) says the
development proves Theorem 1.1 and the growth theorems for through
with no sorry and only the axioms propext, Classical.choice and
Quot.sound, with the axiom audit run as part of its build. The corpus has
not built or audited the development, so the page lists no formalized
evidence.