`Compfiles/Imo2026P4.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

16 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2026, Problem 4

Shan-Yu and Mulan are playing a game. Let θ be an angle with 0° < θ < 180° known to both players. Initially, Shan-Yu makes a paper triangle T with measurements of his choice. Then, they repeatedly perform the following steps:

If T has at least one angle measuring exactly θ, then the game stops and Mulan wins.
Otherwise, Mulan chooses a point P on the perimeter of T, different from its three vertices. She then makes a straight cut from P to the opposite vertex of T, splitting it into two triangles.
Shan-Yu discards one of the two triangles. The remaining triangle becomes the new T.

For which real values of θ can Mulan guarantee her victory in finitely many steps, no matter how Shan-Yu plays?

Statement formalization adapted from AxiomMath/IMO2026; proof adapted from Humanfia's Kimi-K3 solutions (https://github.com/humanfia/imo2026).

Imports (3)

Imported by 1 file

Compfiles.lean

def Imo2026P4.IsTriangle A triangle, viewed as the multiset of its three interior angles (in degrees): positive reals summing to 180 line 47 source
Source documentation
A triangle, viewed as the multiset of its three interior angles (in degrees): positive reals summing to 180.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, Real
Proof uses: And, Eq, Nat, Multiset.card, OfNat.ofNat, Membership.mem, LT.lt, Multiset.sum
9 instances, coercions and auxiliary constants left out.
```
def IsTriangle (s : Multiset ℝ) : Prop :=
…
```
def Imo2026P4.HasAngle A triangle s has an interior angle equal to θ line 51 source
Source documentation
A triangle s has an interior angle equal to θ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Multiset
Proof uses: Membership.mem
1 instances, coercions and auxiliary constants left out.
```
def HasAngle (θ : ℝ) (s : Multiset ℝ) : Prop := θ ∈ s
```
def Imo2026P4.IsCut One admissible cut of the triangle s, producing children L and R line 60 source
Source documentation
One admissible cut of the triangle s, producing children L and R.
We pick an apex angle α and the two base angles β, γ (so s = {α, β, γ}), and a cut parameter x in the open interval (γ, 180 - β). The resulting two triangles have angle multisets L = {β, x, 180 - β - x} and R = {γ, 180 - x, x - γ}. Ranging over all α, β, γ with s = {α, β, γ} captures all three apex choices and both assignments of the two base angles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, Real
Proof uses: Exists, And, Eq, Insert.insert, Singleton.singleton, LT.lt, HSub.hSub, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def IsCut (s L R : Multiset ℝ) : Prop :=
…
```
inductive Imo2026P4.MulanWins The set of triangles from which Mulan can force, in finitely many steps, a triangle with an interior angle equal to θ, no matter how Shan-Yu discards line 75 source
Source documentation
The set of triangles from which Mulan can force, in finitely many steps, a triangle with an interior angle equal to θ, no matter how Shan-Yu discards.
This is the least predicate closed under:
- (win) if the current triangle already has an angle equal to θ, Mulan has won;
- (move) if Mulan can make a cut producing children L and R from both of which she wins (so whichever one Shan-Yu keeps, she still wins), then she wins from the current triangle.
Membership means Mulan wins in finitely many steps.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Multiset
```
inductive MulanWins (θ : ℝ) : Multiset ℝ → Prop
  | win {s : Multiset ℝ} (h : HasAngle θ s) : MulanWins θ s
  | move {s L R : Multiset ℝ} (hcut : IsCut s L R)
      (hL : MulanWins θ L) (hR : MulanWins θ R) : MulanWins θ s

/-- Mulan can guarantee victory for the value `θ`: from every valid starting
triangle she wins in finitely many steps regardless of Shan-Yu's play. -/
```
Mentions: h, Imo2026P4.HasAngle, Imo2026P4.IsCut
def Imo2026P4.MulanCanGuarantee Mulan can guarantee victory for the value θ: from every valid starting triangle she wins in finitely many steps regardless of Shan-Yu's play line 82 source
Source documentation
Mulan can guarantee victory for the value θ: from every valid starting triangle she wins in finitely many steps regardless of Shan-Yu's play.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Multiset, Imo2026P4.IsTriangle, Imo2026P4.MulanWins
```
def MulanCanGuarantee (θ : ℝ) : Prop :=
…
```
lemma Imo2026P4.mem3 Membership in a triple, as a disjunction line 88 source
Source documentation
Membership in a triple, as a disjunction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Membership.mem, Multiset, Insert.insert, Singleton.singleton, Or, Eq
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Multiset.cons, iff_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma mem3 (x a b c : ℝ) : x ∈ ({a, b, c} : Multiset ℝ) ↔ x = a ∨ x = b ∨ x = c := by
…
```
lemma Imo2026P4.rot3 Rotation of a triple line 92 source
Source documentation
Rotation of a triple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Multiset, Insert.insert, Singleton.singleton
Proof uses: id, Eq.mpr, Multiset.cons, congrArg, Multiset.cons_swap, Eq.symm, Multiset.insert_eq_cons, Multiset.pair_comm, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma rot3 (a b c : ℝ) : ({a, b, c} : Multiset ℝ) = {b, c, a} := by
…
```
lemma Imo2026P4.triple_sum Sum of a triple line 98 source
Source documentation
Sum of a triple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Multiset.sum, Insert.insert, Multiset, Singleton.singleton, HAdd.hAdd
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, Multiset.cons, Multiset.sum_cons, Multiset.sum_singleton, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 1 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma triple_sum (a b c : ℝ) : ({a, b, c} : Multiset ℝ).sum = a + b + c := by
…
```
lemma Imo2026P4.triple_card Card of a triple line 103 source
Source documentation
Card of a triple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Nat, Multiset.card, Insert.insert, Multiset, Singleton.singleton, OfNat.ofNat
Proof uses: Iff.mpr, Exists, Multiset.card_eq_three, Exists.intro, rfl
6 instances, coercions and auxiliary constants left out.
```
lemma triple_card (a b c : ℝ) : ({a, b, c} : Multiset ℝ).card = 3 :=
…
```
lemma Imo2026P4.exists_nat_mul_in An open interval of length exceeding θ, with positive left endpoint, contains a positive integer multiple of θ line 108 source
Source documentation
An open interval of length exceeding θ, with positive left endpoint, contains a positive integer multiple of θ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, HAdd.hAdd, Exists, Nat, And, LE.le, HMul.hMul
Proof uses: Int, Int.floor, HDiv.hDiv, Eq.mpr, id, Eq, congrArg, Eq.trans, Int.cast_add, Int.cast_one, Int.lt_floor_add_one, Iff.mp, div_lt_iff₀, Int.floor_le, le_div_iff₀, congrFun', Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 73 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma exists_nat_mul_in (θ : ℝ) (hθ0 : 0 < θ) (u v : ℝ) (hu : 0 < u)
    (huv : u + θ < v) :
    ∃ m : ℕ, 1 ≤ m ∧ u < (m : ℝ) * θ ∧ (m : ℝ) * θ < v := by
…
```
lemma Imo2026P4.good_wins Documented declaration: good_wins line 150 source
Source documentation
A triangle (with sum 180 and positive angles) containing a positive integer multiple k * θ of θ is winning for Mulan, by induction on k: if k ≥ 2, transfer one θ from the apex k * θ to the angle C; the child {C, 180 - C - θ, θ} already contains θ, and the other child contains (k - 1) * θ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Nat, LE.le, Multiset, Membership.mem, HMul.hMul, Eq, Multiset.card, Multiset.sum, Imo2026P4.MulanWins
Proof uses: Nat.le_induction, Imo2026P4.MulanWins.win, Eq.mp, congrArg, Eq.trans, congrFun', Nat.cast_one, one_mul, HAdd.hAdd, Multiset.cons, Exists, Multiset.exists_cons_of_mem, Eq.mpr, id, Multiset.card_cons, Eq.refl, Insert.insert, Singleton.singleton, Iff.mp, Multiset.card_eq_two and 86 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma good_wins (θ : ℝ) (hθ0 : 0 < θ) : ∀ k : ℕ, 1 ≤ k → ∀ s : Multiset ℝ,
    (k : ℝ) * θ ∈ s → s.card = 3 → (∀ y ∈ s, 0 < y) → s.sum = 180 →
    MulanWins θ s := by
…
```
Mentions: Imo2026P4.MulanWins
lemma Imo2026P4.find_cut Documented declaration: find_cut line 208 source
Source documentation
If n * θ = 180 with 2 ≤ n and the triangle {a, b, c} has no angle equal to a positive integer multiple of θ, then some relabeling {A, B, C} of it and some 1 ≤ m satisfy C < m * θ < 180 - B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Nat, LE.le, Eq, HMul.hMul, HAdd.hAdd, Not, Exists, And, Or, Multiset, Insert.insert, Singleton.singleton, HSub.hSub
Proof uses: dite, Imo2026P4.exists_nat_mul_in, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm and 71 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma find_cut (θ : ℝ) (hθ0 : 0 < θ) : ∀ n : ℕ, 2 ≤ n → (n : ℝ) * θ = 180 →
    ∀ a b c : ℝ, 0 < a → 0 < b → 0 < c → a + b + c = 180 →
    (¬∃ k : ℕ, 1 ≤ k ∧ (a = (k : ℝ) * θ ∨ b = (k : ℝ) * θ ∨ c = (k : ℝ) * θ)) →
    ∃ A B C : ℝ, ∃ m : ℕ, ({a, b, c} : Multiset ℝ) = {A, B, C} ∧ 1 ≤ m ∧
      C < (m : ℝ) * θ ∧ (m : ℝ) * θ < 180 - B := by
…
```
lemma Imo2026P4.invariant Documented declaration: invariant line 259 source
Source documentation
Shan-Yu's invariant: assuming 180 is not an integer multiple of θ, for any cut of a sum-180 multiset with no angle an integer multiple of θ, at least one child keeps the same property.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Int, Ne, OfNat.ofNat, Nat, HMul.hMul, Multiset, Eq, Multiset.sum, Membership.mem, Imo2026P4.IsCut, Or, And
Proof uses: Exists, Insert.insert, Singleton.singleton, LT.lt, HSub.hSub, HAdd.hAdd, Eq.mp, congrArg, Imo2026P4.triple_sum, Eq.mpr, id, propext, Imo2026P4.mem3, Or.inl, rfl, Or.inr, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow and 67 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
lemma invariant (θ : ℝ) : (∀ m : ℤ, (180 : ℝ) ≠ (m : ℝ) * θ) →
    ∀ {s L R : Multiset ℝ}, s.sum = 180 →
    (∀ y ∈ s, ∀ k : ℤ, y ≠ (k : ℝ) * θ) → IsCut s L R →
    (L.sum = 180 ∧ ∀ y ∈ L, ∀ k : ℤ, y ≠ (k : ℝ) * θ) ∨
    (R.sum = 180 ∧ ∀ y ∈ R, ∀ k : ℤ, y ≠ (k : ℝ) * θ) := by
…
```
Mentions: Imo2026P4.IsCut
lemma Imo2026P4.not_wins Hence no sum-180 multiset without integer multiples of θ is winning line 306 source
Source documentation
Hence no sum-180 multiset without integer multiples of θ is winning.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Int, Ne, OfNat.ofNat, Nat, HMul.hMul, Multiset, Imo2026P4.MulanWins, Eq, Multiset.sum, Membership.mem, False
Proof uses: Imo2026P4.MulanWins.rec, Imo2026P4.HasAngle, of_eq_true, Eq.trans, True, congrArg, congrFun', Int.cast_one, one_mul, eq_self, Imo2026P4.IsCut, And, Or, Imo2026P4.invariant
33 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma not_wins (θ : ℝ) : (∀ m : ℤ, (180 : ℝ) ≠ (m : ℝ) * θ) → ∀ s : Multiset ℝ,
    MulanWins θ s → s.sum = 180 → (∀ y ∈ s, ∀ k : ℤ, y ≠ (k : ℝ) * θ) → False := by
…
```
Mentions: Imo2026P4.MulanWins
determine Imo2026P4.answer line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Set.ofPred, Exists, Nat, And, LE.le, OfNat.ofNat, Eq, HDiv.hDiv
9 instances, coercions and auxiliary constants left out.
problem Imo2026P4.imo2026_p4 line 328 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Nat, Iff, Imo2026P4.MulanCanGuarantee, Membership.mem, Set, Imo2026P4.answer
Proof uses: id, Iff.intro, Exists, And, LE.le, Eq, HDiv.hDiv, Classical.byContradiction, Not, Int, Ne, HMul.hMul, Decidable.byContradiction, cast, Eq.trans, congrArg, Eq.symm, Nat.cast_zero, Int.cast_zero, Eq.mp and 122 more
167 instances, coercions and auxiliary constants left out.

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