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

70 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2018, Problem 3

An anti-Pascal triangle is an equilateral triangular array of numbers such that, except for the numbers in the bottom row, each number is the absolute value of the difference of the two numbers immediately below it. For example, the following array is an anti-Pascal triangle with four rows which contains every integer from 1 to 10:

4 2 6 5 7 1 8 3 10 9

Does there exist an anti-Pascal triangle with 2018 rows which contains every integer from 1 to 1 + 2 + ... + 2018?

Imports (3)

Imported by 1 file

Compfiles.lean

structure Imo2018P3.Coords line 38 source
no axioms what this means
def Imo2018P3.left_child line 42 source
no axioms what this means
Statement uses: Imo2018P3.Coords
Proof uses: Imo2018P3.Coords.mk, Nat.succ, Imo2018P3.Coords.row, Imo2018P3.Coords.col
def Imo2018P3.right_child line 45 source
no axioms what this means
Statement uses: Imo2018P3.Coords
Proof uses: Imo2018P3.Coords.mk, Nat.succ, Imo2018P3.Coords.row, Imo2018P3.Coords.col
structure Imo2018P3.antipascal_triangle antipascal triangle with n rows line 51 source
Source documentation
antipascal triangle with n rows

no axioms what this means
Statement uses: Nat
```
structure antipascal_triangle (n : ℕ) where
…
```
def Imo2018P3.exists_desired_triangle line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Exists, Imo2018P3.antipascal_triangle, OfNat.ofNat, Nat, LE.le, Finset.sum, Finset.range, HAdd.hAdd, And, LT.lt, Eq, Imo2018P3.antipascal_triangle.f, Imo2018P3.Coords.mk
6 instances, coercions and auxiliary constants left out.
def Imo2018P3.NR Number of rows line 70 source
Source documentation
Number of rows.
```
private def NR : ℕ := 2018
```
def Imo2018P3.TN The total 1 + 2 + ⋯ + 2018 line 73 source
Source documentation
The total 1 + 2 + ⋯ + 2018.
```
private def TN : ℕ := ∑ i ∈ Finset.range NR, (i + 1)
```
Mentions: Imo2018P3.NR
lemma Imo2018P3.NR_val line 75 source
lemma Imo2018P3.TN_def line 77 source
def Imo2018P3.tri The set of cells of an NR-row triangle: row < NR, column ≤ row line 80 source
Source documentation
The set of cells of an NR-row triangle: row < NR, column ≤ row.
```
private def tri : Finset Coords :=
…
```
Mentions: Imo2018P3.Coords
lemma Imo2018P3.mem_tri line 86 source
lemma Imo2018P3.card_tri line 94 source
lemma Imo2018P3.min_sum The sum of n distinct positive integers is at least 1 + 2 + ⋯ + n line 106 source
Source documentation
The sum of n distinct positive integers is at least 1 + 2 + ⋯ + n.
```
private lemma min_sum : ∀ (V : Finset ℕ), (∀ x ∈ V, 1 ≤ x) →
    ∑ i ∈ Finset.range V.card, (i + 1) ≤ ∑ x ∈ V, x := by
…
```
lemma Imo2018P3.min_sum_eq n distinct positive integers with sum at most 1 + 2 + ⋯ + n are exactly {1, …, n} line 134 source
Source documentation
n distinct positive integers with sum at most 1 + 2 + ⋯ + n are exactly {1, …, n}.
```
private lemma min_sum_eq (V : Finset ℕ) (hpos : ∀ x ∈ V, 1 ≤ x) :
    ∑ x ∈ V, x ≤ ∑ i ∈ Finset.range V.card, (i + 1) →
    V = Finset.Icc 1 V.card := by
…
```
lemma Imo2018P3.two_mul_sum line 164 source
lemma Imo2018P3.min_sum_ge The sum of n distinct integers each > m is at least n·m + (1 + ⋯ + n) line 170 source
Source documentation
The sum of n distinct integers each > m is at least n·m + (1 + ⋯ + n).
```
private lemma min_sum_ge (V : Finset ℕ) (m : ℕ) (hpos : ∀ x ∈ V, m < x) :
    V.card * m + ∑ i ∈ Finset.range V.card, (i + 1) ≤ ∑ x ∈ V, x := by
…
```
lemma Imo2018P3.bijection Every cell value lies in [1, TN] and t.f is injective on the triangle line 195 source
Source documentation
Every cell value lies in [1, TN] and t.f is injective on the triangle.
```
private lemma bijection :
    (∀ x ∈ tri, 1 ≤ t.f x ∧ t.f x ≤ TN) ∧ Set.InjOn t.f ↑tri := by
…
```
Mentions: Imo2018P3.tri, Imo2018P3.TN
def Imo2018P3.winner The child of x holding the larger value line 242 source
Source documentation
The child of x holding the larger value.
```
private def winner (x : Coords) : Coords :=
…
```
Mentions: Imo2018P3.Coords
def Imo2018P3.loser The child of x holding the smaller value line 246 source
Source documentation
The child of x holding the smaller value.
```
private def loser (x : Coords) : Coords :=
…
```
Mentions: Imo2018P3.Coords
lemma Imo2018P3.winner_row line 249 source
lemma Imo2018P3.loser_row line 252 source
lemma Imo2018P3.winner_col line 255 source
lemma Imo2018P3.loser_col line 261 source
lemma Imo2018P3.winner_val The defining anti-Pascal relation, oriented: winner = parent + loser line 268 source
Source documentation
The defining anti-Pascal relation, oriented: winner = parent + loser.
```
private lemma winner_val (x : Coords) (hx : x ∈ tri) (hb : x.row + 1 < NR) :
    t.f (winner t x) = t.f x + t.f (loser t x) := by
…
```
Mentions: Imo2018P3.Coords, Imo2018P3.tri, Imo2018P3.NR, Imo2018P3.winner, Imo2018P3.loser
lemma Imo2018P3.left_child_mem Children of a valid parent lie in the triangle line 277 source
Source documentation
Children of a valid parent lie in the triangle.
```
private lemma left_child_mem {x : Coords} (hx : x ∈ tri) (hb : x.row + 1 < NR) :
    left_child x ∈ tri := by
…
```
Mentions: Imo2018P3.Coords, Imo2018P3.tri, Imo2018P3.NR, Imo2018P3.left_child
lemma Imo2018P3.right_child_mem line 282 source
lemma Imo2018P3.winner_mem line 289 source
lemma Imo2018P3.loser_mem line 295 source
def Imo2018P3.chain The greedy "always go to the larger child" path starting at the apex line 302 source
Source documentation
The greedy "always go to the larger child" path starting at the apex.
```
private def chain : ℕ → Coords
  | 0 => ⟨0, 0⟩
  | (i + 1) => winner t (chain i)
```
Mentions: Imo2018P3.Coords, Imo2018P3.winner
lemma Imo2018P3.chain_zero line 306 source
lemma Imo2018P3.chain_succ line 308 source
lemma Imo2018P3.chain_row line 310 source
lemma Imo2018P3.chain_mem line 315 source
lemma Imo2018P3.chain_step_val line 322 source
lemma Imo2018P3.chain_sum line 327 source
def Imo2018P3.losers The smaller children dropped along the apex path (the "losers") line 338 source
Source documentation
The smaller children dropped along the apex path (the "losers").
```
private def losers : Finset Coords :=
…
```
Mentions: Imo2018P3.Coords
def Imo2018P3.smallCells All cells holding a value ≤ NR: the apex together with the losers line 342 source
Source documentation
All cells holding a value ≤ NR: the apex together with the losers.
```
private def smallCells : Finset Coords := insert (chain t 0) (losers t)
```
Mentions: Imo2018P3.Coords, Imo2018P3.chain, Imo2018P3.losers
lemma Imo2018P3.loser_chain_row line 344 source
lemma Imo2018P3.losers_inj line 347 source
lemma Imo2018P3.chain_zero_not_losers line 355 source
lemma Imo2018P3.losers_card line 362 source
lemma Imo2018P3.smallCells_card line 365 source
lemma Imo2018P3.smallCells_subset line 369 source
lemma Imo2018P3.smallCells_sum line 381 source
lemma Imo2018P3.smallCells_injOn line 389 source
lemma Imo2018P3.chain_bottom line 393 source
lemma Imo2018P3.smallCells_image line 412 source
lemma Imo2018P3.not_small Every cell outside the band of small cells holds a value > NR line 429 source
Source documentation
Every cell outside the band of small cells holds a value > NR.
```
private lemma not_small (x : Coords) (hx : x ∈ tri) (hxs : x ∉ smallCells t) :
    NR < t.f x := by
…
```
Mentions: Imo2018P3.Coords, Imo2018P3.tri, Imo2018P3.smallCells, Imo2018P3.NR
lemma Imo2018P3.chain_col_le_succ line 445 source
lemma Imo2018P3.chain_col_succ_le line 448 source
lemma Imo2018P3.chain_col_mono line 451 source
lemma Imo2018P3.chain_col_le_add line 457 source
lemma Imo2018P3.smallCells_col line 467 source
lemma Imo2018P3.notMem_small_left line 490 source
lemma Imo2018P3.notMem_small_right line 495 source
def Imo2018P3.walk A winner-path starting from an arbitrary cell line 503 source
Source documentation
A winner-path starting from an arbitrary cell.
```
private def walk (s : Coords) : ℕ → Coords
  | 0 => s
  | (k + 1) => winner t (walk s k)
```
Mentions: Imo2018P3.Coords, Imo2018P3.winner
lemma Imo2018P3.walk_zero line 507 source
lemma Imo2018P3.walk_succ line 509 source
lemma Imo2018P3.walk_row line 511 source
lemma Imo2018P3.walk_sum line 516 source
def Imo2018P3.inSub Membership in the downward sub-triangle with apex (p, q) line 528 source
Source documentation
Membership in the downward sub-triangle with apex (p, q).
```
private def inSub (p q : ℕ) (x : Coords) : Prop :=
…
```
Mentions: Imo2018P3.Coords
lemma Imo2018P3.inSub_left line 531 source
lemma Imo2018P3.inSub_right line 536 source
lemma Imo2018P3.inSub_winner line 541 source
lemma Imo2018P3.inSub_loser line 547 source
lemma Imo2018P3.walk_inSub line 553 source
lemma Imo2018P3.corner_contra A downward sub-triangle disjoint from the small cells, reaching ≥ 1007 rows down, yields a contradiction: its winner-path picks up ≥ 1007 distinct losers all > NR line 570 source
Source documentation
A downward sub-triangle disjoint from the small cells, reaching ≥ 1007 rows down, yields a contradiction: its winner-path picks up ≥ 1007 distinct losers all > NR.
```
private lemma corner_contra (p q : ℕ) (hp : p ≤ NR - 1)
    (hsub : ∀ x : Coords, inSub p q x → x ∈ tri ∧ x ∉ smallCells t)
    (hlen : 1007 ≤ NR - 1 - p) : False := by
…
```
Mentions: Imo2018P3.NR, Imo2018P3.Coords, Imo2018P3.inSub, Imo2018P3.tri, Imo2018P3.smallCells
lemma Imo2018P3.not_exists_desired line 621 source
determine Imo2018P3.does_exist line 661 source
no axioms what this means
Statement uses: Bool
Proof uses: Bool.false
problem Imo2018P3.imo2018_p3 line 663 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, Eq, Bool, Imo2018P3.does_exist, Bool.true, Imo2018P3.exists_desired_triangle
Proof uses: Eq.mpr, Not, Exists, Imo2018P3.antipascal_triangle, OfNat.ofNat, Nat, LE.le, Finset.sum, Finset.range, HAdd.hAdd, And, LT.lt, Imo2018P3.antipascal_triangle.f, Imo2018P3.Coords.mk, id, Eq.trans, False, congrFun', congrArg, Bool.false_eq_true and 1 more
8 instances, coercions and auxiliary constants left out.

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