---

Claim. Theorem 1.1 (p. 2) of E. Li, A resolution of Erdős Problem 550 on tree versus complete multipartite Ramsey numbers, arXiv:2606.23659v1 (22 June 2026, the date this page is named by), states: "Fix an integer $k\ge2$ and integers $1\le m_1\le\dots\le m_k$. There exists $n_0=n_0(m_1,\dots,m_k)$ such that, for every $n\ge n_0$ and every $n$-vertex tree $T$,

$$R(T,K_{m_1,\dots,m_k})\ \le\ (k-1)\bigl(R(T,K_{m_1,m_2})-1\bigr)+m_1.$$

"

Since $\chi(K_{m_1,\dots,m_k})=k$, this is the inequality of Problem 550 with the class sizes fixed before $n$ grows. With Burr's lower bound $R(T,K_{m_1,\dots,m_k})\ge(k-1)(n-1)+m_1$ the paper states the two-sided form $0\le R(T,F)-((k-1)(n-1)+m_1)\le(k-1)(R(T,K_{m_1,m_2})-n)$ (its (3)). By the paper's own summary (p. 2), the proof runs from the uniform asymptotic $R(T,Q)=(\chi(Q)-1)n+o(n)$ of Erdős, Faudree, Rousseau and Schelp through an off-Turán tree embedding theorem (Szemerédi regularity with the Hladký--Piguet regular-matching lemma), Erdős--Simonovits stability and a compactness-and-rounding theorem for hypergraph obstructions to a counting contradiction (Section 8, p. 19). The statement is recorded on the result page Theorem 1.1 of the library home li_2026_resolution_erdos_problem_550_tree_versus; v1 is the text cited, and v2 (2 August 2026, 26 pages) carries the comment that the proof has been formally verified in Lean.

Submission note. Posted to erdosproblems.com as a proof claim by Eric Li (account EricLi) on 17 July 2026, giving "GPT-5.5 Pro" as the AI used:

We resolve Erdős Problem #550, originally asked as question of Erdős, Faudree, Rousseau, and Schelp. Precisely, for fixed $k\ge2$ and $1\le m_1\le\cdots\le m_k$, we prove that, for every sufficiently large $n$ and every $n$-vertex tree $T$,

$$R\!\left(T,K_{m_1,\ldots,m_k}\right) \le > (k-1)\bigl(R(T,K_{m_1,m_2})-1\bigr)+m_1.$$

The proof combines a new off-Turan

tree-embedding theorem with a compactness-and-rounding theorem for represented bounded-rank hypergraph obstructions. The embedding theorem follows from Szemeredi regularity and a local regular-matching embedding lemma of Hladky and Piguet. The compactness argument uses shadow hypergraphs to retain obstructions whose vertices escape along the limiting sequence.

AI systems. The acknowledgments (v1, p. 20) say that OpenAI's ChatGPT was used for ideation, proof exploration, programming and other work, the author taking full responsibility. The site's proof-claim tab (17 July 2026) gives the claim as made by Eric Li using GPT-5.5 Pro. The Lean repository's formalization.yaml names Harmonic Aristotle, OpenAI ChatGPT and OpenAI Codex as the agents used under the author's direction, and the port's header names Eric Li, Aristotle, OpenAI ChatGPT and OpenAI Codex.

Formalization. Two Lean developments declare themselves formalizations of this theorem: the author's repository ericlisg/erdos550-lean (the first formalization link, at its head of 2 August 2026), and a port of it in Boris Alexeev's repository (the second), which formal-conjectures links as the formal proof of its erdos_550 statement. The community database records that the author's development was rebuilt from a clean clone with only the axioms propext, Classical.choice and Quot.sound. This corpus has built and audited neither, so formalized is not listed.

Depends on. Nothing in this wiki; the proof is the paper's own, with the external inputs it names.

Standing. Claimed. There is no refereed version; the site's curator, T. F. Bloom, wrote in the discussion on 23 June 2026 that Bloom reserves judgement on such proofs until humans have read and vouched for them, and the site's label OPEN (LEAN) keeps the problem open; this corpus has not read the proof or built either Lean development.