`Compfiles/Imo1992P3.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 8 curated AI-written annotations and 3305 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 compfiles documentation, Pinned compfiles corpus index

23 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1992, Problem 3

Consider 9 points in space, no 4 coplanar. Each pair of points is joined by a line segment which is colored either blue or red or left uncolored. Find the smallest value of n such that whenever exactly n edges are colored, the set of colored edges necessarily contains a triangle all of whose edges have the same color.

Imports (3)

Imported by 1 file

Compfiles.lean

structure Imo1992P3.EdgeColoring An edge coloring of the complete graph on 9 vertices by two colors (encoded as Fin 2), where some edges may be left uncolored (none) line 35 source
Source documentation
An edge coloring of the complete graph on 9 vertices by two colors (encoded as Fin 2), where some edges may be left uncolored (none). The vertices are indexed by Fin 9 and the edges by unordered pairs Sym2 (Fin 9); the geometric hypotheses of the problem (9 points in space, no 4 of them coplanar) only serve to guarantee that every pair of points determines an edge, so the problem is purely combinatorial.

no axioms what this means
```
structure EdgeColoring where
…
```
def Imo1992P3.EdgeColoring.coloredEdges The colored edges of an edge coloring, represented as the set of edges that received a color line 44 source
Source documentation
The colored edges of an edge coloring, represented as the set of edges that received a color. (Diagonal "edges" s(i, i) are never colored, so this is exactly the set of colored segments joining two distinct points.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1992P3.EdgeColoring, Finset, Sym2, Fin, OfNat.ofNat, Nat
Proof uses: Finset.filter, Eq, Bool, Option.isSome, Imo1992P3.EdgeColoring.color, Bool.true, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def EdgeColoring.coloredEdges (c : EdgeColoring) : Finset (Sym2 (Fin 9)) :=
…
```
Mentions: Imo1992P3.EdgeColoring
def Imo1992P3.EdgeColoring.uncoloredEdges The uncolored edges of an edge coloring, represented as the set of non-diagonal edges that were left uncolored line 49 source
Source documentation
The uncolored edges of an edge coloring, represented as the set of non-diagonal edges that were left uncolored.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1992P3.EdgeColoring, Finset, Sym2, Fin, OfNat.ofNat, Nat
Proof uses: Finset.filter, And, Eq, Option, Imo1992P3.EdgeColoring.color, Option.none, Not, Sym2.IsDiag, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
def EdgeColoring.uncoloredEdges (c : EdgeColoring) : Finset (Sym2 (Fin 9)) :=
…
```
Mentions: Imo1992P3.EdgeColoring
def Imo1992P3.EdgeColoring.HasMonoTriangle A coloring has a monochromatic triangle if there are three distinct vertices whose three connecting edges all have the same color line 54 source
Source documentation
A coloring has a monochromatic triangle if there are three distinct vertices whose three connecting edges all have the same color.

no axioms what this means
Statement uses: Imo1992P3.EdgeColoring
Proof uses: Exists, Fin, OfNat.ofNat, Nat, And, Ne, Eq, Option, Imo1992P3.EdgeColoring.color, Sym2.mk, Option.some
1 instances, coercions and auxiliary constants left out.
```
def EdgeColoring.HasMonoTriangle (c : EdgeColoring) : Prop :=
…
```
Mentions: Imo1992P3.EdgeColoring
lemma Imo1992P3.fin2_eq_of_ne In Fin 2, two elements different from a common one are equal line 62 source
Source documentation
In Fin 2, two elements different from a common one are equal.

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Eq
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma fin2_eq_of_ne (u v b : Fin 2) (hu : u ≠ b) (hv : v ≠ b) : u = v := by
…
```
lemma Imo1992P3.ramsey6 The Ramsey fact R(3,3) ≤ 6: every red/blue coloring of the edges of the complete graph on 6 vertices contains a monochromatic triangle line 68 source
Source documentation
The Ramsey fact R(3,3) ≤ 6: every red/blue coloring of the edges of the complete graph on 6 vertices contains a monochromatic triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Exists, And, Ne
Proof uses: Finset.card, Finset.erase, Finset.univ, Eq.mpr, HSub.hSub, id, congrArg, Finset.card_erase_of_mem, Finset.mem_univ, Fintype.card, Finset.card_univ, Fintype.card_fin, Eq.refl, Finset.sum, Finset.filter, Finset.card_eq_sum_card_fiberwise, Membership.mem, Set, Finset, LE.le and 62 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma ramsey6 (f : Fin 6 → Fin 6 → Fin 2) (hsym : ∀ i j, f i j = f j i) :
    ∃ i j k : Fin 6, i ≠ j ∧ j ≠ k ∧ k ≠ i ∧ f i j = f j k ∧ f j k = f k i := by
…
```
Mentions: f
def Imo1992P3.minEndpoint The smaller endpoint of an edge, well-defined since min is symmetric line 125 source
Source documentation
The smaller endpoint of an edge, well-defined since min is symmetric.

standard axioms: Quot.sound, propext what this means
Statement uses: Sym2, Fin, OfNat.ofNat, Nat
Proof uses: Equiv, Subtype, Eq, Sym2.lift, Subtype.mk, Min.min
7 instances, coercions and auxiliary constants left out.
```
def minEndpoint (e : Sym2 (Fin 9)) : Fin 9 :=
…
```
lemma Imo1992P3.minEndpoint_mk line 128 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Imo1992P3.minEndpoint, Sym2.mk, Min.min
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
lemma Imo1992P3.mono_triangle_of_colored_ge First part: any coloring with at least 33 colored edges contains a monochromatic triangle line 132 source
Source documentation
First part: any coloring with at least 33 colored edges contains a monochromatic triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1992P3.EdgeColoring, LE.le, Nat, OfNat.ofNat, Finset.card, Sym2, Fin, Imo1992P3.EdgeColoring.coloredEdges, Imo1992P3.EdgeColoring.HasMonoTriangle
Proof uses: Eq, Finset.filter, Not, Sym2.IsDiag, Finset.univ, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Option.isSome, Imo1992P3.EdgeColoring.color, Sym2.ind, False, Sym2.mk, False.elim, Eq.mp, Eq.trans, Bool.false and 66 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 72 steps
Open to load the checked before-and-after goal states.
```
lemma mono_triangle_of_colored_ge (c : EdgeColoring)
    (h : 33 ≤ c.coloredEdges.card) : c.HasMonoTriangle := by
…
```
Mentions: Imo1992P3.EdgeColoring, h
def Imo1992P3.auxColor The extremal coloring on 32 edges (Wöginger's construction): vertices 0,…,3 form the red square, 4,…,7 the blue square, and 8 is the apex line 221 source
Source documentation
The extremal coloring on 32 edges (Wöginger's construction): vertices 0,…,3 form the red square, 4,…,7 the blue square, and 8 is the apex. The diagonals of the two squares are the four uncolored edges.

standard axioms: Quot.sound, propext what this means
Statement uses: Sym2, Fin, OfNat.ofNat, Nat, Option
Proof uses: Equiv, Subtype, Eq, Sym2.lift, Subtype.mk, ite, Option.none, And, LE.le, HMod.hMod, Option.some, Or
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def auxColor : Sym2 (Fin 9) → Option (Fin 2) :=
…
```
lemma Imo1992P3.auxColor_diag line 234 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Option, Imo1992P3.auxColor, Sym2.mk, Option.none
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo1992P3.auxColoring The extremal coloring, packaged as an EdgeColoring line 238 source
Source documentation
The extremal coloring, packaged as an EdgeColoring.

standard axioms: Quot.sound, propext what this means
Statement uses: Imo1992P3.EdgeColoring
Proof uses: Imo1992P3.EdgeColoring.mk, Imo1992P3.auxColor, Imo1992P3.auxColor_diag
```
def auxColoring : EdgeColoring where
…
```
Mentions: Imo1992P3.EdgeColoring
lemma Imo1992P3.aux_colored_card line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Sym2, Fin, OfNat.ofNat, Imo1992P3.EdgeColoring.coloredEdges, Imo1992P3.auxColoring
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1992P3.aux_no_mono line 245 source
standard axioms: Quot.sound, propext what this means
Statement uses: Not, Imo1992P3.EdgeColoring.HasMonoTriangle, Imo1992P3.auxColoring
Proof uses: id, of_decide_eq_true, Exists, Fin, OfNat.ofNat, Nat, And, Ne, Eq, Option, Imo1992P3.EdgeColoring.color, Sym2.mk, Option.some, Bool, Decidable.decide, Bool.true, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo1992P3.shrinkColor Uncoloring the edges of P in the extremal coloring line 250 source
Source documentation
Uncoloring the edges of P in the extremal coloring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Fin, OfNat.ofNat, Nat, Option
Proof uses: ite, Membership.mem, Option.none, Imo1992P3.auxColor
7 instances, coercions and auxiliary constants left out.
```
def shrinkColor (P : Finset (Sym2 (Fin 9))) : Sym2 (Fin 9) → Option (Fin 2) :=
…
```
Mentions: P
lemma Imo1992P3.shrinkColor_apply line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Fin, OfNat.ofNat, Nat, Eq, Option, Imo1992P3.shrinkColor, ite, Membership.mem, Option.none, Imo1992P3.auxColor
Proof uses: rfl
7 instances, coercions and auxiliary constants left out.
lemma Imo1992P3.shrinkColor_diag line 256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Fin, OfNat.ofNat, Nat, Eq, Option, Imo1992P3.shrinkColor, Sym2.mk, Option.none
Proof uses: Eq.mpr, ite, Membership.mem, Imo1992P3.auxColor, id, congrArg, Imo1992P3.shrinkColor_apply, dite, ite_eq_left, Eq.refl, Not, ite_eq_right, Imo1992P3.auxColor_diag
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Imo1992P3.shrinkColoring The shrunk coloring, packaged as an EdgeColoring line 266 source
Source documentation
The shrunk coloring, packaged as an EdgeColoring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Fin, OfNat.ofNat, Nat, Imo1992P3.EdgeColoring
Proof uses: Imo1992P3.EdgeColoring.mk, Imo1992P3.shrinkColor, Imo1992P3.shrinkColor_diag
2 instances, coercions and auxiliary constants left out.
```
def shrinkColoring (P : Finset (Sym2 (Fin 9))) : EdgeColoring where
…
```
Mentions: P, Imo1992P3.EdgeColoring
lemma Imo1992P3.shrinkColor_some_of line 270 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Fin, OfNat.ofNat, Nat, Eq, Option, Imo1992P3.shrinkColor, Option.some, Imo1992P3.auxColor
Proof uses: dite, Membership.mem, False.elim, Eq.mp, Option.none, False, eq_false', noConfusion_of_Nat, Option.ctorIdx, ite, congrArg, ite_eq_left, Imo1992P3.shrinkColor_apply, Not, ite_eq_right
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo1992P3.shrink_coloredEdges line 279 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Fin, OfNat.ofNat, Nat, Eq, Imo1992P3.EdgeColoring.coloredEdges, Imo1992P3.shrinkColoring, SDiff.sdiff, Imo1992P3.auxColoring
Proof uses: Option, Imo1992P3.EdgeColoring.color, Imo1992P3.shrinkColor, rfl, Finset.ext, Eq.mpr, Iff, Membership.mem, Bool, Option.isSome, Bool.true, And, Not, id, congr, congrArg, Eq.trans, Finset.filter, Finset.univ, True and 15 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo1992P3.exists_avoiding Second part: for every m ≤ 32 there is a coloring with exactly m colored edges and no monochromatic triangle line 300 source
Source documentation
Second part: for every m ≤ 32 there is a coloring with exactly m colored edges and no monochromatic triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Imo1992P3.EdgeColoring, And, Eq, Finset.card, Sym2, Fin, Imo1992P3.EdgeColoring.coloredEdges, Not, Imo1992P3.EdgeColoring.HasMonoTriangle
Proof uses: Finset, Imo1992P3.auxColoring, HSub.hSub, Finset.exists_subset_card_eq, Eq.mpr, id, congrArg, Imo1992P3.aux_colored_card, Exists.intro, Imo1992P3.shrinkColoring, And.intro, SDiff.sdiff, Imo1992P3.shrink_coloredEdges, Finset.card_sdiff_of_subset, Nat.sub_sub_self, Eq.refl, Ne, Option, Imo1992P3.EdgeColoring.color, Sym2.mk and 4 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma exists_avoiding (m : ℕ) (hm : m ≤ 32) :
    ∃ c : EdgeColoring, c.coloredEdges.card = m ∧ ¬ c.HasMonoTriangle := by
…
```
Mentions: Imo1992P3.EdgeColoring
determine Imo1992P3.answer line 313 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo1992P3.imo1992_p3 line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Imo1992P3.EdgeColoring, Eq, Finset.card, Sym2, Fin, OfNat.ofNat, Imo1992P3.EdgeColoring.coloredEdges, Imo1992P3.EdgeColoring.HasMonoTriangle, Imo1992P3.answer
Proof uses: Eq.mpr, id, congrArg, rfl, And.intro, Membership.mem, Set, lowerBounds, Imo1992P3.mono_triangle_of_colored_ge, Decidable.byContradiction, LE.le, Not, And, Exists, False, Imo1992P3.exists_avoiding, Eq.mp, LT.lt
15 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.