---

Claim. Let $A(x)$ count the integers $n\le x$ such that every prime $p\mid n$ has a divisor $d>1$ of $n$ with $d\equiv1\pmod p$, the set $A$ of Problem 768. Eric Li's preprint A Resolution of Erdős Problem 768: the Sylow Divisor Condition (arXiv:2606.24872, version 1 of 23 June 2026, version 2 of 13 July 2026) states as its Theorem 1.1 that the limit

$$\lim_{x\to\infty}\frac{\log\bigl(x/A(x)\bigr)}{\sqrt{\log x}\,\log\log x}$$

exists and equals $1/(2\sqrt{\log2})$. That is the asymptotic Erdős asked for, with the constant identified: $A(x)/x=\exp(-(c+o(1))\sqrt{\log x}\log\log x)$ holds with $c=1/(2\sqrt{\log2})$, so the claim answers the question yes. The preprint's route, as its abstract and the site summary describe it: the lower bound (its Theorem 4.3) builds integers from primes placed in disjoint logarithmic intervals and shows that all but a proportion o(1) of them satisfy the condition, through a multiplicative large sieve (its Theorem 2.6) and second- and fourth-moment estimates for subset products; the upper bound (its Theorem 8.3) attaches to each $n$ and each $p\mid n$ its least witness divisor, compresses $n$ by a deterministic map whose fibers are reconstructed injectively, and bounds the result by growing divisor moments. The source card is Li 2026.

Submission note. Posted to erdosproblems.com as a proof claim by Eric Li (account EricLi) on 17 July 2026, giving "GPT-5.5 Pro" as the AI used:

Let $A(x)$ count the positive integers $n\le x$ such that, for every prime $p\mid n$, there is a divisor $d>1$ of $n$ with $d\equiv1\pmod p$. Erdős asked whether

$$\frac{A(x)}x =\exp\!\bigl(-(c+o(1))\sqrt{\log x}\log\log x\bigr) >$$

for some constant $c>0$. We prove that the limit exists and that

$$> \lim_{x\to\infty} \frac{\log(x/A(x))}{\sqrt{\log x}\log\log x} > =\frac1{2\sqrt{\log 2}}.$$

Equivalently, the conjectural asymptotic holds with

$c=1/(2\sqrt{\log 2})$. The lower bound is obtained from primes in disjoint logarithmic intervals using a fourth-moment argument based on the multiplicative large sieve and a subset-product second moment. The upper bound uses canonical witness divisors, a deterministic compression map, an injective reconstruction theorem for its fibers, and growing divisor moments. Thus the paper determines the exact leading constant in Erdős Problem 768. The main theorem and its complete proof have been formally verified with Lean 4. Notes: This paper was also discussed in the comments section before the "proof claim" functionality was added to the website; now it has been added.

Posted to the site's forum by Eric Li on 12 July 2026:

Erdős Problem 768 is resolved, and I have formalised the proof in Lean 4 using Aristotle. In arXiv:2606.24872 I prove that the limit exists:

$\lim_{x\to\infty} \log(x/A(x))/(\sqrt{\log x},\log\log x) = 1/(2\sqrt{\log 2})$.

The formalisation is at github.com/ericlisg/erdos768-lean (tag v1.0.0): the main theorem, Erdos768.erdos_768, is the statement above verbatim, with no sorry in its dependency graph and axioms [propext, Classical.choice, Quot.sound] only, re-verified by CI. The large sieve, subset-product moment, and compression/reconstruction arguments are proved from scratch (~8,500 lines); the PNT input is MediumPNT from PrimeNumberTheoremAnd (a weaker error exponent than the paper's, which suffices - documented in the README, along with reproduction instructions). A statement-level PR to formal-conjectures: #4425.

On the comments above: the paper is not autonomous AI output - the approach and the main ideas are mine, with LLMs pursuing and investigating such ideas under my direction, which I checked and corrected. But Woett is right that nobody should take such an account on trust, and now nobody has to: the proof is complete and the kernel has checked every step of it.

Postings. The arXiv preprint above; the author's Lean 4 repository linked above, pinned to the commit that the forum check below built (the submission itself links the repository root), which the preprint says proves Theorem 1.1 as a hypothesis-free declaration Erdos768.erdos_768 with no sorry, drawing its prime number theorem input from the PrimeNumberTheoremAnd project, and which the preprint's reference [8] also cites as an archived release, version 1.0.0, Zenodo, DOI 10.5281/zenodo.21326350; and the full proof claim on the site's proof-claim tab, submitted 17 July 2026 and recorded there as made using GPT-5.5 Pro, whose note says the paper had been discussed in the problem's comment thread before the tab existed. In that thread the author posted the result on 12 July 2026 and announced the formalization at its tag v1.0.0. On 14 July 2026 Johan Land posted an independent Lean development of Li's proof, linked above, which presents itself as Li's proof machine-checked. It was written from the preprint without Li's code and, Land's post says, with extensive use of AI, and Land says they did no human review of the proof. Land reported a small missing hypothesis in the preprint's Lemma 6.3, which counts the formal records, and called it immaterial with a trivial fix. Land's development repairs it, and Li's formalization does not have the slip. The author thanked Land the same day and said a third version would reflect it; the arXiv record lists only versions 1 and 2. Neither development was built or audited here. The preprint's own statement on the use of artificial intelligence says that large language models, primarily OpenAI's ChatGPT, were used extensively throughout the research, with the author originating the ideas and evaluating the outputs, and that the Lean formalization was produced with Harmonic's Aristotle, directed and audited by the author. The site summary restates the theorem and the two bounds.

Acceptance. None on record. The site's label is OPEN and its page was last edited 14 September 2025, before the preprint, so the curator had not acted on the claim when the proof-claim tab was accessed. The two comments on the claim are a forum user's report of 17 July 2026 that a fresh clone of the repository built from source on the official toolchain and that an independently written axiom check of the main theorem reported only propext, Classical.choice and Quot.sound, with the definitions matching the site's statement, and the author's reply; a forum comment is neither a named reviewer nor a referee, so it is not listed as evidence. No journal record was found: the arXiv record carried no journal reference. Neither formalization is listed either: nothing was cloned, built or audited here, and no statement-fidelity review exists in this corpus. The claim stays claimed, and the problem's standing is claimed, proved, through this page.

Depends on. No page of this wiki.