Wiki
Wiki

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

Updated


Claim. With n0(f,α)n_0(f,\alpha) the least integer such that every n≥n0n\ge n_0 is f(a1)+⋯+f(ar)f(a_1)+\cdots+f(a_r) over distinct positive integers aia_i with 1a1+⋯+1ar=α\frac1{a_1}+\cdots+\frac1{a_r}=\alpha, 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 α=1\alpha=1: n0(x+b,1)≤172+10bn_0(x+b,1)\le172+10b for every integer 1≤b≤50001\le b\le5000 (Theorem 3); n0(5x+b,1)≤20000n_0(5x+b,1)\le20000 for every integer 1≤b<3751\le b<375 not divisible by 55 (Theorem 4); and n0(x2+b,1)≤50000n_0(x^2+b,1)\le50000 for every integer 1≤b≤8001\le b\le800 (Theorem 5), each theorem also covering one or two further rationals α\alpha. 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 f(x)=axd+bf(x)=ax^d+b with coprime coefficients and any positive rational α\alpha, the existence of n0(f,α)n_0(f,\alpha) to a finite computation: finite sets AiA_i of denominators with prescribed reciprocal sums and ff-sums, together with representations of all nn in a bounded interval of each residue class, propagate to all large nn 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 p(x)=x+5p(x)=x+5 and p(x)=x2+100p(x)=x^2+100.

Covers. The linear polynomials x+bx+b (1≤b≤50001\le b\le5000), the polynomials 5x+b5x+b (1≤b<3751\le b<375, 5∤b5\nmid b) and the quadratic polynomials x2+bx^2+b (1≤b≤8001\le b\le800), 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.