Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to the particular question of Problem 781 is no: there are constants with
for all (Theorem 1.1 of N. Alon and J. Spencer, Ascending waves, stated in the introduction), so fails for every large , and is determined up to constant factors, which settles the estimate asked for. The paper states that it settles the problem of Brown, Erdős and Freedman, who asked whether the lower bound is the exact value. The upper bound is the greedy argument of the paper's introduction, sharpened by Brown, Erdős and Freedman to (Theorem 4, Section 4; the site displays the same bound), and their coloring in blocks of lengths gives ; their closing remarks (Section 5) already record Spencer and Alon's announcement of the matching lower bound . Library homes: alon_1989_ascending_waves (the page rests on the statement and the introduction; no proof check of the lower bound is recorded) and brown_1990_quasi_progressions_descending_waves.
Depends on. Nothing in this wiki.
Acceptance. Refereed: J. Combin. Theory Ser. A 52 (1989), no. 2,
275--287, doi:10.1016/0097-3165(89)90033-2; the Crossref record dates the
issue to November 1989, filled to the first of the month for this page's
name. Reviewed: the site's curator, Thomas Bloom, credits the resolution to
Alon and Spencer in the problem page's commentary and labels the problem
disproved (accessed 2026-10-07; no last-edited date; the community database
lists the problem as disproved as of its last update on 2025-08-31); its
discussion thread and proof-claim tab were empty. A Lean 4 development,
src/latest/ErdosProblems/Erdos781.lean of Boris Alexeev's lean-proofs
repository (3,223 lines at the pinned commit of 2026-09-15, first added
2026-08-17), declares itself a formalization of a solution to the problem:
its header names Alon and Spencer as informal authors and Codex and GPT-5.6
Sol as formal authors, and its erdos_781 proves that
and for all and that does not
hold for all , with the minimal defined in the file as waveRamsey;
it closes with #print axioms erdos_781 without the printed output. The
formal-conjectures statement for the problem (commit of 2026-09-20) is
tagged solved in both its parts and names line 3202 of the file, the
theorem, as their formal proof. The corpus has not built the development, so
the page lists no formalized evidence. Nothing here rests on a review by
this project.