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

14 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2000, Problem 4

Find the smallest positive integer $n$ such that if $n$ squares of a $1000 \times 1000$ chessboard are colored, then there will exist three colored squares whose centers form a right triangle with sides parallel to the edges of the board.

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2000P4.Good Documented declaration: Good line 34 source
Source documentation
A set S of squares on an m × n board contains no forbidden triangle: one cannot find three (distinct) chosen squares whose centers form a right triangle with sides parallel to the edges of the board, that is, with two of them in the same row and two of them in the same column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin
Proof uses: Membership.mem, Ne, Not, And, Or, Eq, Prod.fst, Prod.snd
2 instances, coercions and auxiliary constants left out.
```
def Good {m n : ℕ} (S : Finset (Fin m × Fin n)) : Prop :=
…
```
Mentions: S
def Usa2000P4.rowFiber The squares of S lying in row r line 41 source
Source documentation
The squares of S lying in row r.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin
Proof uses: Finset.filter, Eq, Prod.fst
1 instances, coercions and auxiliary constants left out.
```
def rowFiber {m n : ℕ} (S : Finset (Fin m × Fin n)) (r : Fin m) : Finset (Fin m × Fin n) :=
…
```
Mentions: S
def Usa2000P4.colFiber The squares of S lying in column c line 45 source
Source documentation
The squares of S lying in column c.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin
Proof uses: Finset.filter, Eq, Prod.snd
1 instances, coercions and auxiliary constants left out.
```
def colFiber {m n : ℕ} (S : Finset (Fin m × Fin n)) (c : Fin n) : Finset (Fin m × Fin n) :=
…
```
Mentions: S
lemma Usa2000P4.mem_rowFiber line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, Iff, Membership.mem, Usa2000P4.rowFiber, And, Eq, Prod.fst
Proof uses: Finset.mem_filter
3 instances, coercions and auxiliary constants left out.
lemma Usa2000P4.mem_colFiber line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, Iff, Membership.mem, Usa2000P4.colFiber, And, Eq, Prod.snd
Proof uses: Finset.mem_filter
3 instances, coercions and auxiliary constants left out.
lemma Usa2000P4.Good.mono Any subset of a good set is good line 55 source
Source documentation
Any subset of a good set is good.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, LE.le, Usa2000P4.Good
Proof uses: Membership.mem
8 instances, coercions and auxiliary constants left out.
```
lemma Good.mono {m n : ℕ} {S T : Finset (Fin m × Fin n)} (hTS : T ⊆ S) (hS : Good S) :
    Good T :=
…
```
Mentions: S, Usa2000P4.Good
lemma Usa2000P4.alone_of_good Documented declaration: alone_of_good line 63 source
Source documentation
In a good set, every chosen square is the unique chosen square of its row or the unique chosen square of its column: otherwise the square together with a different chosen square in its row and a different chosen square in its column would form a forbidden configuration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, Usa2000P4.Good, Membership.mem, Or, Eq, Prod.fst, Prod.snd
Proof uses: Decidable.byContradiction, Not, Exists, And, Ne, False, Eq.mp, Eq.trans, congr, congrArg, Mathlib.Tactic.Push.not_forall_eq, funext, Prod.ext, Ne.symm, And.intro, Or.inl, Eq.symm, Or.inr
17 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma alone_of_good {m n : ℕ} {S : Finset (Fin m × Fin n)} (hS : Good S)
    {s : Fin m × Fin n} (hs : s ∈ S) :
    (∀ t ∈ S, t.1 = s.1 → t = s) ∨ (∀ t ∈ S, t.2 = s.2 → t = s) := by
…
```
Mentions: S, Usa2000P4.Good
lemma Usa2000P4.good_of_alone Documented declaration: good_of_alone line 79 source
Source documentation
Conversely, if every square of S is alone in its row or alone in its column, then S is good: in any would-be forbidden triple, the row-pair and the column-pair share a square, which then has both a row-partner and a column-partner.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, Membership.mem, Or, Eq, Prod.fst, Prod.snd, Usa2000P4.Good
Proof uses: Ne, And, False, Eq.symm, absurd, Prod.ext, Ne.symm
6 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma good_of_alone {m n : ℕ} {S : Finset (Fin m × Fin n)}
    (h : ∀ s ∈ S, (∀ t ∈ S, t.1 = s.1 → t = s) ∨ (∀ t ∈ S, t.2 = s.2 → t = s)) :
    Good S := by
…
```
Mentions: S, h, Usa2000P4.Good
lemma Usa2000P4.card_le_of_good Upper bound: a good set on an m × n board with m, n ≥ 2 has at most m + n - 2 squares line 111 source
Source documentation
Upper bound: a good set on an m × n board with m, n ≥ 2 has at most m + n - 2 squares.
Proof: call a row (resp. column) light if it contains exactly one chosen square and heavy if it contains at least two. The squares lying in light rows are in bijection with the light rows, and every square in a heavy row is the unique chosen square of its column (by alone_of_good), so the squares in heavy rows inject into the light columns. Hence |S| ≤ (#light rows) + (#light columns). If there is at least one heavy row and one heavy column, this is at most m + n - 2; if there is no heavy row then |S| ≤ m, and if there is no heavy column then |S| ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Prod, Fin, Usa2000P4.Good, Finset.card, HSub.hSub, HAdd.hAdd
Proof uses: Finset.image, Prod.fst, Eq, rfl, Prod.snd, Finset.filter, Usa2000P4.rowFiber, Usa2000P4.colFiber, Membership.mem, And, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Eq.mpr, id, Eq.symm, Iff.mpr, LT.lt and 48 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 169 steps
Open to load the checked before-and-after goal states.
```
lemma card_le_of_good {m n : ℕ} (hm : 2 ≤ m) (hn : 2 ≤ n)
    {S : Finset (Fin m × Fin n)} (hS : Good S) :
    S.card ≤ m + n - 2 := by
…
```
Mentions: S, Usa2000P4.Good
def Usa2000P4.construction The extremal configuration: every square of row 0 or of column 0, except the corner square (0, 0) line 281 source
Source documentation
The extremal configuration: every square of row 0 or of column 0, except the corner square (0, 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Fin, OfNat.ofNat, Nat
Proof uses: Union.union, SProd.sprod, Singleton.singleton, Finset.erase, Finset.univ
10 instances, coercions and auxiliary constants left out.
```
def construction : Finset (Fin 1000 × Fin 1000) :=
…
```
lemma Usa2000P4.card_construction Documented declaration: card_construction line 289 source
Source comment
The `constructorNameAsVariable` linter normalizes the types of all binders; here those are memberships in concrete finsets on the `1000 × 1000` board, whose `whnf` unfolds a 1000-element list and exceeds the recursion limit.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Prod, Fin, OfNat.ofNat, Usa2000P4.construction
Proof uses: SProd.sprod, Finset, Singleton.singleton, Finset.erase, Finset.univ, Eq.mpr, HMul.hMul, id, congrArg, Finset.card_product, Finset.card_singleton, HSub.hSub, Finset.card_erase_of_mem, Finset.mem_univ, Fintype.card, Finset.card_univ, Fintype.card_fin, Eq.refl, Disjoint, Membership.mem and 16 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma card_construction : construction.card = 1998 := by
…
```
lemma Usa2000P4.good_construction See the comment at card_construction for the disabled linter line 312 source
Source comment
See the comment at `card_construction` for the disabled linter.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2000P4.Good, OfNat.ofNat, Nat, Usa2000P4.construction
Proof uses: Eq, Finset, Prod, Fin, Union.union, SProd.sprod, Singleton.singleton, Finset.erase, Finset.univ, rfl, Usa2000P4.good_of_alone, Membership.mem, And, Prod.fst, Prod.snd, Or, Eq.mp, congrArg, propext, Finset.mem_product and 11 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma good_construction : Good construction := by
…
```
Mentions: Usa2000P4.Good, Usa2000P4.construction
determine Usa2000P4.smallestN line 345 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Usa2000P4.usa2000_p4 line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Finset, Prod, Fin, OfNat.ofNat, Eq, Finset.card, Not, Usa2000P4.Good, Usa2000P4.smallestN
Proof uses: And.intro, Membership.mem, Set, lowerBounds, LE.le, HSub.hSub, HAdd.hAdd, Usa2000P4.card_le_of_good, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Decidable.byContradiction, LT.lt, Nat.lt_of_not_le, And, Usa2000P4.construction, Exists, False and 7 more
25 instances, coercions and auxiliary constants left out.

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