Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Problem 88 asks, for every , for a such that a graph on vertices with no clique or independent set of size at least has an induced subgraph with exactly edges for every . Kwan, Sah, Sauermann and Sawhney prove it in a stronger form. Their Theorem 1.1 states that for fixed and and large in terms of them, every -Ramsey graph on vertices (no homogeneous subgraph of size ) has, for every integer , a vertex subset inducing exactly edges. The paper's footnote 2 derives the conjecture in its form from the case through the Erdős--Szemerédi density bound for -Ramsey graphs. The theorem is deduced from Theorem 1.2, an anticoncentration bound of order for the edge count of a random vertex subset, together with the Alon--Krivelevich--Sudakov theorem for small edge counts.
Scope. Full. The deduction from the theorem to the site's exact wording follows the footnote. Read the site's logarithm in any fixed base : a graph with no clique or independent set of size at least is -Ramsey for , which depends on alone. By Erdős and Szemerédi, as the footnote quotes it, every -Ramsey graph on vertices with large in terms of has . Let be at least the threshold of Theorem 1.1 for and at least the threshold of that density bound, and put . For every integer lies in the theorem's range; for , , so the only such is , the empty subgraph. The footnote's own version takes and handles small the same way (); only the base change is added here. Erdős's original hypothesis of edges is implied by the other condition, as the site's commentary and the footnote both note.
Depends on. Nothing in this wiki; the deduction above is the only step beyond the cited paper.
Acceptance. Reviewed: the site's curator, T. F. Bloom, labels the problem PROVED, with the note that the answer is yes, and credits the solution to the four authors in the problem's commentary (page accessed 2026-09-18); the thread and the proof-claim tab are empty. The site's credit line thanks Mehtaab Sawhney, one of the four authors; the PROVED label and the credit in the commentary are the curator's, and the refereed publication stands independently. Refereed: the paper is published in Forum of Mathematics, Pi 11 (2023), e21, DOI 10.1017/fmp.2023.17 (published online 24 August 2023; Crossref record accessed). The text read is the arXiv v2 of 30 May 2024, posted after the journal publication; the journal text is not held and was not compared with it. The claims of Theorem 1.1, footnote 2 and Theorem 1.2 are checked and the proof is not; nothing here is independently reviewed.
Postings. arXiv:2208.02874, v1 of 4 August 2022 (the first posting,
which dates this page) and v2 of 30 May 2024, the version read; the
journal article; the site's problem page, whose thread and proof-claim tab
were empty on 2026-09-18. Boris Alexeev's lean-proofs repository holds
Erdos88.lean (first committed 21 August 2026, linked above at its commit of
15 September 2026). Its header declares it a Lean formalization of a
solution to Problem 88, with Kwan, Sah, Sauermann and Sawhney as informal
authors and Codex and GPT-5.6 Sol as formal authors. Its theorem
erdos_88 states the site's form, for every , with the natural
logarithm. This corpus has not built it, so it adds no formalized evidence.