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 with , where is the least number of distinct divisors of that always suffice to write every positive integer below as a sum. This answers the first question of Problem 18, the one carrying the prize, in the affirmative with exponent , and would improve on Vose's , the best accepted bound for infinitely many practical . 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 for infinitely many practical numbers , thereby answering affirmatively the question whether for infinitely many practical .
Covers. The first question only: infinitely many practical with . The claim concerns general practical and says nothing about , 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.