550.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/550
[Ch77] Chvátal, V., Tree-complete graph Ramsey numbers. J. Graph Theory (1977), 93.
[Li26] Li, E., A Resolution of Erdős Problem 550 on Tree versus Complete Multipartite Ramsey Numbers, arXiv:2606.23659 (2026).

Imports (1)

theorem Erdos550.erdos_550 sorry line 50 source
depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Monotone, LT.lt, Filter.Eventually, SimpleGraph, SimpleGraph.IsTree, SimpleGraph.graphRamsey, Sigma, SimpleGraph.completeMultipartiteGraph, HAdd.hAdd, HMul.hMul, HSub.hSub, Sum, Fin.mk, completeBipartiteGraph, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.