Cross-Reference Redirection

Cross-Reference Redirection

Table of Contents

	Introduction
	Background: Ramsey numbers, formalized
	The shape of the proof
	Why three pages occupy 2 700 lines
	Lemma 1 — Erdős–Szekeres `R(k, ℓ) ≤ C(k+ℓ-2, k-1)`
	Lemma 2 — the probabilistic lower bound
	Lemma 3 — dependent random choice
	Putting it together
	The squeeze: from quantitative to `Tendsto`
	Capstone: the headline statement, type-checked here
	Reproduce it
	References
	Acknowledgements