Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The manuscript, titled "Minimum Ramsey numbers for graphs with a prescribed number of edges", asserts that
a bound the claimant attributes to Sudakov as a conjecture and claims to prove. The lower bound is said to come from the early stage of the triangle-free process, with a martingale estimate showing that no graph of high enough density embeds at that stage, and a passage to subgraphs that disposes of a maximum-degree hypothesis. The tab lists the claim under Qiyuan Gu's name; it was submitted on 10 September 2026 by the account AlexErdosProblem. For Problem 1182 the claimant deduces , the order of the 1980 lower bound of Burr, Erdős, Faudree, Rousseau and Schelp, and, since is known, counts the orders of both functions as determined.
Submission note. Posted to erdosproblems.com as a proof claim by Qiyuan Gu (account fireflysentinel) on 10 September 2026, giving "GPT 6 Astra" as the AI used:
We prove min₍e(G)=m₎ R(K₃,G) = Θ(m^(2/3)/(log m)^(1/3)), settling a conjecture of Sudakov. The lower bound is obtained from the early triangle-free process, using a martingale estimate to avoid every embedding of a sufficiently dense graph, together with a subgraph reduction removing the maximum-degree assumption. For Erdős Problem 1182, this gives f(n)=Θ(n^(3/2)√log n). Since the other quantity was already known to satisfy F(n)=Θ(n), this determines the order of magnitude of both functions in Problem 1182 and completes the problem. Notes: GPT-6 Astra was used to propose the mathematical proofs and generate the Lean formalization. GPT-5.6 Sol and Claude Opus 5 were used for editorial review of the exposition. The author finished the final manuscript and takes full responsibility for its content.
Scope. Full, as the claimant states it: the problem asks to estimate and , and the claim fixes the order of while taking the order of from the literature. The closing question about is answered no by the pending claim Brandt 1996.
Depends on. Brandt 1996 for the upper half of ; the lower half, and the lower bound on whose order the claim asserts, are Burr, Erdős, Faudree, Rousseau and Schelp 1980.
Standing. Claimed. The Zenodo record was published on 10 September 2026 with
an anonymous creator field and a description consisting of the problem's URL,
and its related identifiers cite Sudakov's 2007 paper; the manuscript is not
compiled here and nothing of the argument is checked, so no evidence kind is
listed. The claim's notes on the site say that GPT-6 Astra proposed the proofs
and generated a Lean formalization, that GPT-5.6 Sol and Claude Opus 5 reviewed
the exposition, and that the author finished the manuscript and takes
responsibility for it; the tab names the claim as made using GPT 6 Astra. The
Zenodo record carries a Lean archive (erdos-1182-lean.zip) beside the PDF, not
built here; it is linked above as the formalization, and no formalization is
linked from the tab. The attribution is provenance only. The tab says that a
listing there does not mean the site has examined the proof; the claim has no
comments, and the site's label (OPEN, page last edited 11 April 2026) and its
commentary are unchanged. The claim is accepted neither by the site nor by a
named mathematician; if correct, it would close the factor that
Sudakov 2007 leaves
between the 1980 lower bound and Sudakov's upper bound, showing the 1980 lower
bound for to have the right order.