Wiki
Wiki

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

min⁡e(G)=mR(K3,G)=Θ ⁣(m2/3(log⁡m)1/3),\min_{e(G)=m}R(K_3,G)=\Theta\!\left(\frac{m^{2/3}}{(\log m)^{1/3}}\right),

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 f(n)=Θ(n3/2(log⁡n)1/2)f(n)=\Theta(n^{3/2}(\log n)^{1/2}), the order of the 1980 lower bound of Burr, Erdős, Faudree, Rousseau and Schelp, and, since F(n)=Θ(n)F(n)=\Theta(n) 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 f(n)f(n) and F(n)F(n), and the claim fixes the order of f(n)f(n) while taking the order of F(n)F(n) from the literature. The closing question about F(n)/nF(n)/n is answered no by the pending claim Brandt 1996.

Depends on. Brandt 1996 for the upper half of F(n)=Θ(n)F(n)=\Theta(n); the lower half, and the lower bound on f(n)f(n) 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 (log⁡n)1/2(\log n)^{1/2} that Sudakov 2007 leaves between the 1980 lower bound and Sudakov's upper bound, showing the 1980 lower bound for f(n)f(n) to have the right order.