Erdős 557

Read formalization.yaml

method

other — Claude (Anthropic)

review

other — mechanically verified (lean kernel, standard axioms only; see ci); no independent mathematical refereeing

sorry

0 unproved goals declared

sources

Erdős problem #557 (erdosproblems.com) — background; On partition theorems for finite graphs — background; The Erdős-Sós conjecture in dense graphs — background; Erdős problem #548 (Erdős–Sós conjecture): proof — builds-on

related

tadamcz/erdos548/blob/82ffb751f3d37768927df9239ed08439bbe0dd09/Challenge.lean — builds-on

divergences

The informal problem asks whether R_k(T) ≤ kn + O(1) for every tree T on n vertices. `erdos_557` states this with an absolute constant c (c = 3 is exhibited), which is the strongest reading of O(1) (it does not depend on k). A k-colouring of the edges of K_m is modelled by Mathlib's `TopEdgeLabeling (Fin m) (Fin k)`, a function from the edge set of the complete graph to `Fin k`; a monochromatic copy is `T.IsContained (C.labelGraph i)` (not necessarily induced). `multicolourRamsey k G` is the infimum of the set of m for which every such labelling has a monochromatic copy of G; by `Nat.sInf_le` the explicit theorem gives the bound. Trees with n ≥ 1 vertices are covered; for n = 0 there are no trees (`IsTree` requires a vertex). The value k = 0 is allowed and degenerate: no 0-labelling of a graph with an edge exists.

checked by

nobody independent of its authors yet