Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 351
claims/: The 3 claim pages of Problem 351, one per claimant's result; the problem's standing derives from them.
Statement. Let with positive leading coefficient. Is it true that
is strongly complete, in the sense that, for any finite set ,
contains all sufficiently large integers?
Status. Proved, in the site's label "PROVED (LEAN)". The argument that GPT 5.5 Pro produced for Problem 283, posted on 2026-05-03 by Liam Price and edited by Kevin Barreto, yields the statement for every with positive leading coefficient; Nat Sothanaphan confirmed it with ChatGPT, it is formalized in Lean, and the site accepted it (page last edited 10 May 2026). See the claim page. Earlier partial results, each with its own claim page: Graham [Gr63] for (accepted, refereed) and van Doorn's note of 2025-09-15 deducing from Graham's method and Alekseyev [Al19] (claimed). The (Lean) suffix of the site's label PROVED (LEAN) means nothing here: this corpus has not built or audited the Lean proof.
Source. erdosproblems.com/351, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #351, https://www.erdosproblems.com/351.
References.
- [Al19] Alekseyev, Max A., On partitions into squares of distinct integers whose reciprocals sum to 1. (2019), 213-221.
- [Gr63] Graham, R. L., A theorem on partitions. J. Austral. Math. Soc. (1963), 435-441.
- [Gr64f] Graham, R. L., Complete sequences of polynomial values. Duke Math. J. (1964), 275-285.
Formalization. Statement in
formal-conjectures
at the file's last change (2026-09-18), whose formal_proof attribute points
to a Lean wrapper of the Problem 283 development; the claim page pins the
proof files.
Progress
Not yet compiled.
Known Results
Not yet compiled.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- graham_1964_complete_sequences_polynomial_values
- alekseyev_2019_partitions_into_squares_distinct_integers_whose
- alekseyev_2019_partitions_into_squares_distinct_integers_whose / theorem_1
- graham_1963_theorem_partitions
- graham_1963_theorem_partitions / theorem_1
- graham_1963_theorem_partitions / theorem_2