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

22 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1974, Problem 4

Consider decompositions of an 8 × 8 chessboard into p non-overlapping rectangles, subject to the following conditions:

(i) Each rectangle has as many white squares as black squares. (ii) If aᵢ is the number of white squares in the i-th rectangle, then a₁ < a₂ < ... < aₚ.

Find the maximum value of p for which such a decomposition is possible. For this value of p, determine all possible sequences a₁, a₂, ..., aₚ.

Imports (8)

Imported by 1 file

Compfiles.lean

structure Imo1974P4.Rect A rectangle on the chessboard, given by the coordinates (r, c) of its top-left unit square, its height h (number of rows) and its width w (number of columns) line 41 source
Source documentation
A rectangle on the chessboard, given by the coordinates (r, c) of its top-left unit square, its height h (number of rows) and its width w (number of columns).

no axioms what this means
```
structure Rect where
…
```
def Imo1974P4.Rect.cells The unit squares making up a rectangle line 49 source
Source documentation
The unit squares making up a rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1974P4.Rect, Finset, Prod, Nat
Proof uses: Finset.Icc, Prod.fst, Prod.snd, Prod.mk, Imo1974P4.Rect.r, Imo1974P4.Rect.c, HAdd.hAdd, HSub.hSub, Imo1974P4.Rect.h, OfNat.ofNat, Imo1974P4.Rect.w
12 instances, coercions and auxiliary constants left out.
```
def Rect.cells (R : Rect) : Finset (ℕ × ℕ) :=
…
```
Mentions: Imo1974P4.Rect
def Imo1974P4.isWhite The white squares of the chessboard are those whose coordinates have even sum line 54 source
Source documentation
The white squares of the chessboard are those whose coordinates have even sum.

no axioms what this means
Statement uses: Prod, Nat
Proof uses: Eq, HMod.hMod, HAdd.hAdd, Prod.fst, Prod.snd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def isWhite (x : ℕ × ℕ) : Prop :=
…
```
instance Imo1974P4.(instance at line 57) line 57 source
def Imo1974P4.Rect.whiteCount The number of white squares of a rectangle line 61 source
Source documentation
The number of white squares of a rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1974P4.Rect, Nat
Proof uses: Finset.card, Prod, Finset.filter, Imo1974P4.isWhite, Imo1974P4.Rect.cells
1 instances, coercions and auxiliary constants left out.
```
def Rect.whiteCount (R : Rect) : ℕ :=
…
```
Mentions: Imo1974P4.Rect
def Imo1974P4.Rect.blackCount The number of black squares of a rectangle line 65 source
Source documentation
The number of black squares of a rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1974P4.Rect, Nat
Proof uses: Finset.card, Prod, Finset.filter, Not, Imo1974P4.isWhite, Imo1974P4.Rect.cells
2 instances, coercions and auxiliary constants left out.
```
def Rect.blackCount (R : Rect) : ℕ :=
…
```
Mentions: Imo1974P4.Rect
def Imo1974P4.board The 8 × 8 chessboard line 69 source
Source documentation
The 8 × 8 chessboard.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Nat
Proof uses: Finset.Icc, Prod.fst, Prod.snd, Prod.mk, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def board : Finset (ℕ × ℕ) :=
…
```
def Imo1974P4.ValidDecomp Documented declaration: ValidDecomp line 77 source
Source documentation
A valid decomposition of the chessboard: a finite set of nonempty rectangles contained in the board, pairwise disjoint, covering the whole board, each having as many white squares as black squares (condition (i)), and such that no two rectangles have the same number of white squares (condition (ii)).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo1974P4.Rect
Proof uses: And, Membership.mem, LE.le, Nat, OfNat.ofNat, Imo1974P4.Rect.h, Imo1974P4.Rect.w, HAdd.hAdd, Imo1974P4.Rect.r, Imo1974P4.Rect.c, Ne, Eq, Prod, Inter.inter, Imo1974P4.Rect.cells, EmptyCollection.emptyCollection, Finset.biUnion, Imo1974P4.board, Imo1974P4.Rect.whiteCount, Imo1974P4.Rect.blackCount and 2 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def ValidDecomp (T : Finset Rect) : Prop :=
…
```
Mentions: Imo1974P4.Rect
instance Imo1974P4.(instance at line 84) line 84 source
determine Imo1974P4.solutions line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
5 instances, coercions and auxiliary constants left out.
determine Imo1974P4.maxCount The maximum possible number of white squares line 93 source
Source documentation
The maximum possible number of white squares.

no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
determine maxCount : ℕ := 7
…
```
lemma Imo1974P4.Rect.card_cells The number of unit squares of a rectangle is the product of its two side lengths line 99 source
Source documentation
The number of unit squares of a rectangle is the product of its two side lengths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1974P4.Rect, LE.le, Nat, OfNat.ofNat, Imo1974P4.Rect.h, Imo1974P4.Rect.w, Eq, Finset.card, Prod, Imo1974P4.Rect.cells, HMul.hMul
Proof uses: Finset, SProd.sprod, Finset.Icc, Imo1974P4.Rect.r, HAdd.hAdd, HSub.hSub, Imo1974P4.Rect.c, rfl, Eq.mpr, id, congrArg, Finset.card_product, Nat.card_Icc, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma Rect.card_cells (R : Rect) (hh : 1 ≤ R.h) (hw : 1 ≤ R.w) :
    R.cells.card = R.h * R.w := by
…
```
Mentions: Imo1974P4.Rect
lemma Imo1974P4.Rect.whiteCount_add_blackCount White and black squares together make up all squares of a rectangle line 110 source
Source documentation
White and black squares together make up all squares of a rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1974P4.Rect, Eq, Nat, HAdd.hAdd, Imo1974P4.Rect.whiteCount, Imo1974P4.Rect.blackCount, Finset.card, Prod, Imo1974P4.Rect.cells
Proof uses: id, Finset.card_filter_add_card_filter_not, Imo1974P4.isWhite
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Rect.whiteCount_add_blackCount (R : Rect) :
    R.whiteCount + R.blackCount = R.cells.card := by
…
```
Mentions: Imo1974P4.Rect
lemma Imo1974P4.Rect.one_le_whiteCount A rectangle satisfying condition (i) has at least one white square line 117 source
Source documentation
A rectangle satisfying condition (i) has at least one white square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1974P4.Rect, LE.le, Nat, OfNat.ofNat, Imo1974P4.Rect.h, Imo1974P4.Rect.w, Eq, Imo1974P4.Rect.whiteCount, Imo1974P4.Rect.blackCount
Proof uses: Finset.card, Prod, Imo1974P4.Rect.cells, HMul.hMul, Imo1974P4.Rect.card_cells, HAdd.hAdd, Imo1974P4.Rect.whiteCount_add_blackCount, Nat.mul_le_mul
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma Rect.one_le_whiteCount (R : Rect) (hh : 1 ≤ R.h) (hw : 1 ≤ R.w)
    (hbal : R.whiteCount = R.blackCount) : 1 ≤ R.whiteCount := by
…
```
Mentions: Imo1974P4.Rect
lemma Imo1974P4.card_mul_succ_le_two_mul_sum A finite set of k distinct positive integers has sum at least `1 + 2 + line 126 source
Source documentation
A finite set of k distinct positive integers has sum at least 1 + 2 + ... + k, here phrased as k * (k + 1) ≤ 2 * ∑ x ∈ S, x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Membership.mem, LE.le, OfNat.ofNat, HMul.hMul, Finset.card, HAdd.hAdd, Finset.sum
Proof uses: Finset.strongInduction, LT.lt, Eq, EmptyCollection.emptyCollection, Finset.Nonempty, Or, Finset.eq_empty_or_nonempty, of_eq_true, Eq.trans, True, congr, congrArg, zero_add, mul_one, MulZeroClass.mul_zero, Eq.symm, And, id, Exists, Finset.exists_max_image and 44 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma card_mul_succ_le_two_mul_sum (S : Finset ℕ) :
    (∀ x ∈ S, 1 ≤ x) → S.card * (S.card + 1) ≤ 2 * ∑ x ∈ S, x := by
…
```
Mentions: S
lemma Imo1974P4.sum_whiteCount The total number of white squares in a valid decomposition is 32 line 154 source
Source documentation
The total number of white squares in a valid decomposition is 32.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo1974P4.Rect, Imo1974P4.ValidDecomp, Eq, Nat, Finset.sum, Imo1974P4.Rect.whiteCount, OfNat.ofNat
Proof uses: Membership.mem, And, LE.le, Imo1974P4.Rect.h, Imo1974P4.Rect.w, HAdd.hAdd, Imo1974P4.Rect.r, Imo1974P4.Rect.c, Ne, Prod, Inter.inter, Imo1974P4.Rect.cells, EmptyCollection.emptyCollection, Finset.biUnion, Imo1974P4.board, Imo1974P4.Rect.blackCount, Finset.card, Finset.image, Set.PairwiseDisjoint, Finset.filter and 22 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma sum_whiteCount (T : Finset Rect) (hT : ValidDecomp T) :
    ∑ R ∈ T, R.whiteCount = 32 := by
…
```
Mentions: Imo1974P4.Rect, Imo1974P4.ValidDecomp
lemma Imo1974P4.seven_distinct_sum_32 The five sets of seven distinct positive integers summing to 32 line 177 source
Source documentation
The five sets of seven distinct positive integers summing to 32. (Enumerated by decide over the 7-subsets of [1, 11].)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Finset.card, OfNat.ofNat, Membership.mem, LE.le, Finset.sum, Insert.insert, Singleton.singleton
Proof uses: Finset.powersetCard, Finset.Icc, Iff.mpr, And, Finset.mem_powersetCard, And.intro, Finset.mem_Icc, Finset.filter, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Finset.mem_filter, Eq.mp, congrArg
23 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma seven_distinct_sum_32 (S : Finset ℕ) (hcard : S.card = 7)
    (hpos : ∀ x ∈ S, 1 ≤ x) (hmax : ∀ x ∈ S, x ≤ 11) (hsum : ∑ x ∈ S, x = 32) :
    S ∈ ({{1, 2, 3, 4, 5, 6, 11}, {1, 2, 3, 4, 5, 7, 10},
          {1, 2, 3, 4, 5, 8, 9}, {1, 2, 3, 4, 6, 7, 9},
          {1, 2, 3, 5, 6, 7, 8}} : Finset (Finset ℕ)) := by
…
```
Mentions: S
def Imo1974P4.decomp₁ A decomposition realising the white-square counts {1, 2, 3, 4, 5, 7, 10} (rectangle sizes 2, 4, 6, 8, 10, 14, 20) line 198 source
Source documentation
A decomposition realising the white-square counts {1, 2, 3, 4, 5, 7, 10} (rectangle sizes 2, 4, 6, 8, 10, 14, 20).

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Imo1974P4.Rect
Proof uses: Insert.insert, Imo1974P4.Rect.mk, OfNat.ofNat, Nat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def decomp₁ : Finset Rect :=
…
```
Mentions: Imo1974P4.Rect
def Imo1974P4.decomp₂ A decomposition realising the white-square counts {1, 2, 3, 4, 5, 8, 9} (rectangle sizes 2, 4, 6, 8, 10, 16, 18) line 204 source
Source documentation
A decomposition realising the white-square counts {1, 2, 3, 4, 5, 8, 9} (rectangle sizes 2, 4, 6, 8, 10, 16, 18).

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Imo1974P4.Rect
Proof uses: Insert.insert, Imo1974P4.Rect.mk, OfNat.ofNat, Nat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def decomp₂ : Finset Rect :=
…
```
Mentions: Imo1974P4.Rect
def Imo1974P4.decomp₃ A decomposition realising the white-square counts {1, 2, 3, 4, 6, 7, 9} (rectangle sizes 2, 4, 6, 8, 12, 14, 18) line 210 source
Source documentation
A decomposition realising the white-square counts {1, 2, 3, 4, 6, 7, 9} (rectangle sizes 2, 4, 6, 8, 12, 14, 18).

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Imo1974P4.Rect
Proof uses: Insert.insert, Imo1974P4.Rect.mk, OfNat.ofNat, Nat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def decomp₃ : Finset Rect :=
…
```
Mentions: Imo1974P4.Rect
def Imo1974P4.decomp₄ A decomposition realising the white-square counts {1, 2, 3, 5, 6, 7, 8} (rectangle sizes 2, 4, 6, 10, 12, 14, 16) line 216 source
Source documentation
A decomposition realising the white-square counts {1, 2, 3, 5, 6, 7, 8} (rectangle sizes 2, 4, 6, 10, 12, 14, 16).

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Imo1974P4.Rect
Proof uses: Insert.insert, Imo1974P4.Rect.mk, OfNat.ofNat, Nat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def decomp₄ : Finset Rect :=
…
```
Mentions: Imo1974P4.Rect
problem Imo1974P4.imo1974_p4 line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Finset, Imo1974P4.Rect, Imo1974P4.ValidDecomp, LE.le, Nat, Finset.card, Imo1974P4.maxCount, Eq, Membership.mem, Imo1974P4.solutions, Finset.image, Imo1974P4.Rect.whiteCount, Exists
Proof uses: And.intro, OfNat.ofNat, Imo1974P4.Rect.h, Imo1974P4.Rect.w, HAdd.hAdd, Imo1974P4.Rect.r, Imo1974P4.Rect.c, Ne, Prod, Inter.inter, Imo1974P4.Rect.cells, EmptyCollection.emptyCollection, Finset.biUnion, Imo1974P4.board, Imo1974P4.Rect.blackCount, Finset.injOn_of_card_image_eq, Finset.sum, Eq.mpr, id, congrArg and 48 more
56 instances, coercions and auxiliary constants left out.

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