Formal evidence
The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
Combinatorics · formal theorem
Erdős–Szekeres Monotone Subsequence Theorem
Any injective sequence of r · s + 1 values in a linear order contains either a strictly increasing subsequence of length r + 1 or a strictly decreasing one of length s + 1.
Scope: The finite monotone-subsequence theorem for injective finite sequences over a linear order.
Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Exact formal proposition
Hypotheses and conclusion
This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.
def ErdosSzekeresMonotoneStatement : Prop :=
∀ (α : Type) [LinearOrder α] (r s : Nat)
(a : Fin (r * s + 1) → α),
Function.Injective a →
HasStrictIncreasingSubsequence a (r + 1) ∨
HasStrictDecreasingSubsequence a (s + 1)Definitions used in this proposition
HasStrictIncreasingSubsequence
def HasStrictIncreasingSubsequence {α : Type} [Preorder α] {n : Nat}
(a : Fin n → α) (k : Nat) : Prop :=
∃ idx : Fin k → Fin n, StrictMono idx ∧ StrictMono (fun i => a (idx i))HasStrictDecreasingSubsequence
def HasStrictDecreasingSubsequence {α : Type} [Preorder α] {n : Nat}
(a : Fin n → α) (k : Nat) : Prop :=
∃ idx : Fin k → Fin n, StrictMono idx ∧ StrictAnti (fun i => a (idx i))Lean wrapper declaration
The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.
theorem erdosSzekeresMonotone :
ErdosSzekeresMonotoneStatementThe theorem at a glance
Erdős–Szekeres at a glance
Accessible transcript
Injective a : Fin (r*s+1) → α ⇒ increasing length r+1 ∨ decreasing length s+1
Assign each index the lengths of the longest increasing and decreasing subsequences ending there. If both desired outcomes failed, r·s + 1 indices would have to occupy only r·s distinct rank pairs, giving the pigeonhole contradiction. This is the finite monotone-subsequence theorem, not the geometric happy-ending theorem.
Read the complete poster transcript
FINITE COMBINATORICS · ORDER THEORY
ERDŐS–SZEKERES MONOTONE SUBSEQUENCE
r·s + 1
DISTINCT TERMS FORCE A MONOTONE SUBSEQUENCE
FOR EVERY LINEAR ORDER · r,s ∈ N · INJECTIVE a
STRICTLY INCREASING · LENGTH r + 1
OR
STRICTLY DECREASING · LENGTH s + 1
A subsequence keeps the original index order.
INDEX · VALUE
STRICTLY INCREASING (LENGTH r + 1)
STRICTLY DECREASING (LENGTH s + 1)
RANK GRID · r × s
Rows = increasing rank (1 to r)
Columns = decreasing rank (1 to s)
THE EXTRA INDEX (IMPOSSIBLE TO PLACE)
HOW THE PROOF MOVES
1 · ASSIGN TWO RANKS
Longest increasing and decreasing endings at each index.
2 · ASSUME BOTH OUTCOMES FAIL
Every rank pair lies in an r × s grid.
3 · SEPARATE EVERY INDEX
Distinct indices receive distinct rank pairs.
4 · PIGEONHOLE CONTRADICTION
r·s + 1 indices cannot fit into r·s rank pairs.
EXACT SCOPE
Finite injective sequences in a linear order.
Not the geometric happy-ending theorem. No claim about consecutive terms.
Theorem schematic
One sequence, two forced directions
r·s + 1 terms ⇒ increasing length r + 1 ∨ decreasing length s + 1
One injective sequence in a linear order is the only input. The rank-pair argument selects indices in their original order and forces either r + 1 strictly increasing values or s + 1 strictly decreasing values; it does not require consecutive terms.
Result boundary
What this theorem does—and does not—establish
The finite monotone-subsequence theorem for injective finite sequences over a linear order.
- This is not the geometric happy-ending theorem.
- This is not a finite-search-only result.
- This accepted-result record does not establish novelty and does not by itself authorize public export or deployment.
About these visual explanations
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
Open questions and extensions
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
What the source ZIP contains
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Publication review
Review record
Publication reviews accepted
Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.
Statement alignment
The formal declaration was accepted against the named theorem and its exact variant.
Result boundary
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
Public wording
The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
Canonical source
The first-party source link is pinned to the checked package commit and exact Lean file.
Accepted result
A validated accepted-result record binds the four reviews to the checked formalization.