---

Claim. The theorem Erdos547.erdos_547 of the Lean development linked above states that there is $n_0$ such that for every $n\ge n_0$, every tree $T$ on Fin n and every simple graph $G$ on Fin (2 * n - 2), $T$ is contained in $G$ or in its complement: every two-coloring of $K_{2n-2}$ has a monochromatic copy of every tree on $n\ge n_0$ vertices, that is $R(T)\le2n-2$. The file's module comment describes its route through the Gallai--Edmonds decomposition, regularity and the embedding of small trees, and it does not follow a named paper. The same file proves Erdos547.not_erdos_547, the failure of the site's wording at $n=1$, which the problem page credits in its Notes and which counts for nothing. The file was added to Boris Alexeev's repository of Lean proofs of Erdős problems on 2026-08-26 and is linked at the commit that holds it.

Covers. The corrected Statement of Problem 547 for every tree on $n\ge n_0$ vertices, with $n_0$ not explicit. The finitely many orders below $n_0$ are outside this claim; the full corrected Statement is settled by the accepted claim page [[problems/ramsey_theory/E0547/claims/2026_09_03_adamczewski|the 2026 claim]].

Standing. The file names no author, so the claim is recorded under the repository owner's slug. No outside reviewer has examined it and this corpus has not built or audited it, so it carries no formalized evidence and stays claimed. The same repository's Erdos547b.lean formalizes Zhao's theorem and is a link on the Zhao page.

Depends on. No page of this wiki.