Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to
Problem 763 is no: for no
and no constant is
. The claimed result is the theorem of
H. L. Montgomery and R. C. Vaughan, On the Erdős–Fuchs theorems, in the
form the site's commentary records: for the summatory representation
count cannot equal . This
sharpens Theorem 1 of Erdős and Fuchs
(their claim page)
from the error term to ; the site
credits the improvement to Jurkat, in unpublished work, and to Montgomery
and Vaughan. A bounded error term is in particular , so the
theorem answers the question on its own. The library holds no copy; the
statement follows the site's commentary and the formal-conjectures variant
erdos_763.variants.montgomery_vaughan, which states it without proof.
Depends on. Nothing in this wiki.
Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the
problem DISPROVED and credits the improved error term to
Jurkat and to Montgomery and Vaughan in the problem page's commentary (the
proof-claim tab is empty and the thread has no posts). The paper
appeared in A Tribute to Paul Erdős, Cambridge Univ. Press (1990),
331--338, doi:10.1017/CBO9780511983917.025, an edited volume whose
refereeing is not documented, so no refereed evidence is listed; the
Crossref record gives only the year, so the page carries
the first day of it. The Lean 4 development
src/latest/ErdosProblems/Erdos763.lean of Boris Alexeev's lean-proofs
repository (first added 2026-08-17; formal authors Codex and GPT-5.6 Sol)
names Montgomery and Vaughan, with Erdős and Fuchs, as informal authors of
the solution it formalizes, and its not_erdos_763 proves the
bounded-error case only, not the error term; the corpus has
not built it, so the page lists no formalized evidence.