This is a proof of the Erdős–Szekeres theorem formalized in Lean, an interactive theorem prover. The theorem says that
Any sequence of real numbers with length at least (r − 1)(s − 1) + 1 contains a monotonically increasing subsequence of length r or a monotonically decreasing subsequence of length s.
The corresponding statement in Lean is
theorem erdos_szekeres
{X : Type*} [linear_order X]
(A : list X)
(r s : ℕ)
(h : (r-1)*(s-1) < A.length)
: (∃ (R : list X), R <+ A ∧ R.length = r ∧ R.pairwise (≤))
∨ (∃ (S : list X), S <+ A ∧ S.length = s ∧ S.pairwise (≥))Note that the theorem has been generalized to any linear order, not just the real numbers.
There is also another version stated using an ordered finset instead of list.
theorem erdos_szekeres''
{X Y: Type*} [linear_order X] [linear_order Y]
(r s : ℕ)
(A : finset X)
(h : (r-1)*(s-1) < A.card)
(f : X → Y)
: (∃ R ⊆ A, R.card = r ∧ ∀ (x ∈ R) (y ∈ R), x ≤ y → f x ≤ f y)
∨ (∃ S ⊆ A, S.card = s ∧ ∀ (x ∈ S) (y ∈ S), x ≤ y → f y ≤ f x)The axiom of choice has not been avoided.