Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. There are infinitely many practical nn with h(n)≪(log⁡log⁡n)2h(n)\ll(\log\log n)^2, where h(n)h(n) is the least number of distinct divisors of nn that always suffice to write every positive integer below nn as a sum. This answers the first question of Problem 18, the one carrying the prize, in the affirmative with exponent 22, and would improve on Vose's h(m)≪(log⁡m)1/2h(m)\ll(\log m)^{1/2}, the best accepted bound for infinitely many practical mm. Liam Price submitted the claim on the problem's proof-claims tab on 24 July 2026 as a partial proof found with GPT-5.6 Sol Pro; the human submitter is the claimant here and the system is named as the claim names it. The write-up, "Sparse Divisor Sums", sits behind an Overleaf read link (second link) that this corpus did not obtain, so its statement is known from the claim's summary and from the thread. The thread's comment of 6 August 2026 identifies the analytic input as Bourgain's multilinear exponential-sum theorem for arbitrary moduli (J. Anal. Math. 106 (2008)), whose size hypothesis the earlier announcement omits, and the combinatorial core as a modular-lifting lemma. The same comment reports a third-party Lean certification of the elementary layer, in the repository scottdhughes/erdos18-lean-certification (15 theorems, Lean v4.32.2), whose README says that it certifies no solution; it formalizes lemmas and not the result, so it is not a formalization link. The card is price_2026_sparse_divisor_sums.

Submission note. Posted to erdosproblems.com as a proof claim by Liam Price (account Leeham) on 24 July 2026, giving "GPT 5.6 Sol Pro" as the AI used:

GPT-5.6 Sol Pro proves that h(n)≪(log⁡log⁡n)2h(n)\ll(\log\log n)^2 for infinitely many practical numbers nn, thereby answering affirmatively the question whether h(n)<(log⁡log⁡n)O(1)h(n)<(\log\log n)^{O(1)} for infinitely many practical nn.

Covers. The first question only: infinitely many practical nn with h(n)<(log⁡log⁡n)O(1)h(n)<(\log\log n)^{O(1)}. The claim concerns general practical nn and says nothing about h(n!)h(n!), so the second and third questions are untouched.

Depends on. No page of this wiki.

Standing. The claim is claimed. The claim was posted as partial (the tab heads it as a proof claim) and the site shows the problem open; its curator has not accepted it, no refereed publication exists, and no Lean proof of the full argument is known. An explicit elementary version of the same bound, presented by its authors as a simplification of this argument, is van Doorn and GPT-6 Astra Pro's claim, recorded separately because it is a different proof with a different analytic input.