Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. With the least integer such that every
is over distinct positive integers with
, Wouter van Doorn's manuscript The
binomial case of Graham's conjecture on polynomial representations with
prescribed sum of reciprocals (11 pages; a PDF in the author's GitHub
repository Woett/A-normal-paper-is-probably-fine, linked from the site's
thread on 31 August 2025 as work in progress, the linked copy being the file
of 24 March 2026) states, for : for every
integer (Theorem 3); for every integer
not divisible by (Theorem 4); and for
every integer (Theorem 5), each theorem also covering one or
two further rationals . For these polynomials the question of
Problem 283 is therefore answered
yes with an explicit threshold. The theorems rest on the manuscript's
Theorems 1 and 2, which reduce, for with coprime coefficients
and any positive rational , the existence of to a
finite computation: finite sets of denominators with prescribed
reciprocal sums and -sums, together with representations of all in
a bounded interval of each residue class, propagate to all large by a
scaling-and-shift mechanism modeled on the author's earlier work. The
problem page's Partial results and the site's commentary cite the manuscript
for the examples and .
Covers. The linear polynomials (), the polynomials (, ) and the quadratic polynomials (), each with the stated threshold. For every other polynomial the manuscript decides nothing: its reduction gives a finite computation whose completion for a given binomial it does not assert. The general case is the full claim Price 2026.
Depends on. Nothing in this wiki; the reduction and the computations are the manuscript's own.
Formalization. The author's file ErdosProblem283.lean in the repository
Woett/Lean-files, at the pinned commit of the first formalization link,
declares itself generated by Aristotle (Harmonic) and a formalization of the
manuscript named above; it proves two theorems, meta_theorem and
general_theorem, the reduction of Theorems 1 and 2, in 610 lines without
sorry, ending with #print axioms commands for both theorems whose output the
file does not record; the re-hosted copy records propext, Classical.choice
and Quot.sound for both. Boris Alexeev's repository plby/lean-proofs
re-hosts it as Erdos283b.lean at the pinned commit of the second
formalization link (936 lines), with van Doorn as informal author, Aristotle
and van Doorn as formal authors, and the status partial: it formalizes the
reduction, not the computations of Theorems 3--5. The formal-conjectures
statement file for the problem records the linear and quadratic families as the
variants van_doorn_linear and van_doorn_quadratic with sorry bodies; a
statement file is not a formalization and is not linked. This corpus has built
and audited none of these files, so the claim lists no formalized evidence.
Standing. Claimed. The manuscript is unrefereed, is not on arXiv and
has no journal record; the author presents it as work in progress. The
site's commentary records that van Doorn proved the conjecture for many
linear and quadratic polynomials, but the problem's label, PROVED (LEAN),
settles the whole problem through the Price argument rather than these
cases, so the curator's credit is not reviewed evidence. Read depth: the
theorem statements are checked against the linked PDF; the proofs and the
computations are not verified.