RamseyNumbers.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

19 declarations, 15 contain sorry, 0 declared as axioms

Ramsey numbers

The (graph) Ramsey number $R(k,\ell)$ is the least natural number $n$ such that every simple graph on $n$ vertices contains either a clique of size $k$ or an independent set of size $\ell$ (equivalently, the complement graph contains a clique of size $\ell$).

We formalize the classical open problem of determining $R(5,5)$, together with the currently best known bounds $43 \le R(5,5) \le 46$.

Note: the diagonal Ramsey number $R(n,n)$ can also be formulated in terms of 2-colorings of $2$-subsets, as Combinatorics.hypergraphRamsey 2 n (see FormalConjecturesForMathlib/Combinatorics/Ramsey.lean).

References:

Wikipedia: Ramsey number
[Rad] S. P. Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1. (Updated periodically.) https://www.combinatorics.org/ojs/index.php/eljc/article/view/DS1
[Exoo89] G. Exoo, A lower bound for $R(5,5)$, Journal of Graph Theory 13 (1989), 97–98. DOI: 10.1002/jgt.3190130113
[AM24] V. Angeltveit and B. McKay, $R(5,5) \le 46$, arXiv:2409.15709 (2024).
OEIS A212954
MathWorld: Ramsey Number

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

def RamseyNumbers.IsGraphRamsey Documented declaration: IsGraphRamsey line 54 source
Source documentation
IsGraphRamsey n k l means that for every simple graph G on n vertices, either
- G contains a clique of size k, or
- the complement graph Gᶜ contains a clique of size l (equivalently, G contains an independent set of size l).
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SimpleGraph, Fin, Not, And, SimpleGraph.CliqueFree, Compl.compl
1 instances, coercions and auxiliary constants left out.
```
def IsGraphRamsey (n k l : ℕ) : Prop :=
…
```
theorem RamseyNumbers.IsGraphRamsey.succ Monotonicity in the number of vertices line 59 source
Source documentation
Monotonicity in the number of vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, RamseyNumbers.IsGraphRamsey, HAdd.hAdd, OfNat.ofNat
Proof uses: SimpleGraph, Fin, SimpleGraph.comap, Function.Embedding, Fin.castSuccEmb, SimpleGraph.Embedding, SimpleGraph.Embedding.comap, Compl.compl, Equiv.toFun, SimpleGraph.Embedding.complEquiv, And, SimpleGraph.CliqueFree, False, SimpleGraph.CliqueFree.comap, SimpleGraph.Embedding.isContained, And.intro
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem IsGraphRamsey.succ (n k l : ℕ) :
    IsGraphRamsey n k l → IsGraphRamsey (n + 1) k l := by
…
```
Mentions: RamseyNumbers.IsGraphRamsey
theorem RamseyNumbers.IsGraphRamsey.symm Symmetry in the clique / independent set sizes line 73 source
Source documentation
Symmetry in the clique / independent set sizes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, RamseyNumbers.IsGraphRamsey
Proof uses: Iff.intro, SimpleGraph, Fin, Eq.mpr, Not, And, SimpleGraph.CliqueFree, Compl.compl, SimpleGraph.IndepSetFree, id, Eq, Eq.trans, congrArg, Eq.mp, congr, congrFun', compl_compl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem IsGraphRamsey.symm (n k l : ℕ) :
    IsGraphRamsey n k l ↔ IsGraphRamsey n l k := by
…
```
Mentions: RamseyNumbers.IsGraphRamsey
theorem RamseyNumbers.classicalRamsey_eq_sInf The shared Ramsey number agrees with the clique-free formulation line 81 source
Source documentation
The shared Ramsey number agrees with the clique-free formulation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, SimpleGraph.classicalRamsey, InfSet.sInf, Set.ofPred, RamseyNumbers.IsGraphRamsey
Proof uses: of_eq_true, SimpleGraph, Fin, Or, SimpleGraph.IsContained, SimpleGraph.completeGraph, Compl.compl, Eq.trans, True, congrArg, Set, funext, Not, And, SimpleGraph.CliqueFree, forall_congr, congr, eq_self
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem classicalRamsey_eq_sInf (k l : ℕ) :
    SimpleGraph.classicalRamsey k l = sInf {n : ℕ | IsGraphRamsey n k l} := by
…
```
Mentions: SimpleGraph.classicalRamsey, RamseyNumbers.IsGraphRamsey
theorem RamseyNumbers.ramsey_number_five_five The open problem: determine the Ramsey number $R(5,5)$ sorry line 96 source
Source documentation
The open problem: determine the Ramsey number $R(5,5)$.
It is known that $43 \le R(5,5) \le 46$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_five_five :
    R(5, 5) = answer(sorry) := by
…
```
theorem RamseyNumbers.ramsey_number_five_five_lower_bound Lower bound $43 \le R(5,5)$, equivalently: there exists a graph on $42$ vertices with no $5$-clique and no independent set of size $5$ sorry line 105 source
Source documentation
Lower bound $43 \le R(5,5)$, equivalently: there exists a graph on $42$ vertices with no $5$-clique and no independent set of size $5$.

depends on sorry what this means
Statement uses: Exists, SimpleGraph, Fin, OfNat.ofNat, Nat, And, SimpleGraph.CliqueFree, Compl.compl
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_five_five_lower_bound :
    ∃ G : SimpleGraph (Fin 42), G.CliqueFree 5 ∧ (Gᶜ).CliqueFree 5 := by
…
```
theorem RamseyNumbers.ramsey_number_five_five_upper_bound Upper bound $R(5,5) \le 46$, i.e. every graph on $46$ vertices contains a $5$-clique or an independent set of size $5$ sorry line 114 source
Source documentation
Upper bound $R(5,5) \le 46$, i.e. every graph on $46$ vertices contains a $5$-clique or an independent set of size $5$.

depends on sorry what this means
Statement uses: RamseyNumbers.IsGraphRamsey, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_five_five_upper_bound :
    IsGraphRamsey 46 5 5 := by
…
```
Mentions: RamseyNumbers.IsGraphRamsey
theorem RamseyNumbers.ramsey_number_three_three $R(3,3) = 6$ sorry line 127 source
Source documentation
$R(3,3) = 6$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_three_three : R(3, 3) = 6 := by
…
```
theorem RamseyNumbers.ramsey_number_three_four $R(3,4) = 9$ sorry line 132 source
Source documentation
$R(3,4) = 9$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_three_four : R(3, 4) = 9 := by
…
```
theorem RamseyNumbers.ramsey_number_three_five $R(3,5) = 14$ sorry line 137 source
Source documentation
$R(3,5) = 14$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_three_five : R(3, 5) = 14 := by
…
```
theorem RamseyNumbers.ramsey_number_three_six $R(3,6) = 18$ sorry line 142 source
Source documentation
$R(3,6) = 18$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_three_six : R(3, 6) = 18 := by
…
```
theorem RamseyNumbers.ramsey_number_three_seven $R(3,7) = 23$ sorry line 147 source
Source documentation
$R(3,7) = 23$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_three_seven : R(3, 7) = 23 := by
…
```
theorem RamseyNumbers.ramsey_number_three_eight $R(3,8) = 28$ sorry line 152 source
Source documentation
$R(3,8) = 28$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_three_eight : R(3, 8) = 28 := by
…
```
theorem RamseyNumbers.ramsey_number_three_nine $R(3,9) = 36$ (Grinstead–Roberts) sorry line 157 source
Source documentation
$R(3,9) = 36$ (Grinstead–Roberts).

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_three_nine : R(3, 9) = 36 := by
…
```
theorem RamseyNumbers.ramsey_number_four_four The diagonal Ramsey number $R(4,4) = 18$ sorry line 162 source
Source documentation
The diagonal Ramsey number $R(4,4) = 18$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_four_four : R(4, 4) = 18 := by
…
```
theorem RamseyNumbers.ramsey_number_four_five $R(4,5) = 25$ (McKay–Radziszowski) sorry line 167 source
Source documentation
$R(4,5) = 25$ (McKay–Radziszowski).

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_four_five : R(4, 5) = 25 := by
…
```
theorem RamseyNumbers.ramsey_number_six_six The diagonal Ramsey number $R(6,6)$ is unknown sorry line 175 source
Source documentation
The diagonal Ramsey number $R(6,6)$ is unknown. The best known bounds recorded in [Rad] are $102 \le R(6,6) \le 165$.

depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.classicalRamsey, OfNat.ofNat, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_six_six : R(6, 6) = answer(sorry) := by
…
```
theorem RamseyNumbers.ramsey_number_six_six_lower_bound Lower bound $102 \le R(6,6)$, equivalently: there exists a graph on $101$ vertices with no $6$-clique and no independent set of size $6$ sorry line 183 source
Source documentation
Lower bound $102 \le R(6,6)$, equivalently: there exists a graph on $101$ vertices with no $6$-clique and no independent set of size $6$.

depends on sorry what this means
Statement uses: Exists, SimpleGraph, Fin, OfNat.ofNat, Nat, And, SimpleGraph.CliqueFree, Compl.compl
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_six_six_lower_bound :
    ∃ G : SimpleGraph (Fin 101), G.CliqueFree 6 ∧ (Gᶜ).CliqueFree 6 := by
…
```
theorem RamseyNumbers.ramsey_number_six_six_upper_bound Upper bound $R(6,6) \le 165$, i.e. every graph on $165$ vertices contains a $6$-clique or an independent set of size $6$ sorry line 192 source
Source documentation
Upper bound $R(6,6) \le 165$, i.e. every graph on $165$ vertices contains a $6$-clique or an independent set of size $6$.

depends on sorry what this means
Statement uses: RamseyNumbers.IsGraphRamsey, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ramsey_number_six_six_upper_bound :
    IsGraphRamsey 165 6 6 := by
…
```
Mentions: RamseyNumbers.IsGraphRamsey