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

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1971, Problem 6

Let $A = (a_{ij})$ be an $n \times n$ matrix with non-negative integer entries. Suppose that for all $i, j$, if $a_{ij} = 0$, then the sum of the elements in the $i$-th row plus the sum of the elements in the $j$-th column is at least $n$. Prove that the sum of all elements in the matrix is at least $n^2 / 2$.

Imports (3)

Imported by 1 file

Compfiles.lean

def Imo1971P6.rowSum Definitions of row sum, column sum, and total sum line 36 source
Source comment
Definitions of row sum, column sum, and total sum

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin
Proof uses: Finset.sum, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
def rowSum (i : Fin n) : ℕ := ∑ j, A i j
```
def Imo1971P6.colSum line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin
Proof uses: Finset.sum, Finset.univ, Matrix.transpose
2 instances, coercions and auxiliary constants left out.
def Imo1971P6.totalSum line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin
Proof uses: Finset.sum, Finset.univ
2 instances, coercions and auxiliary constants left out.
lemma Imo1971P6.totalSum_eq_rowSum_sum Basic lemmas connecting total sum to row/col sums line 41 source
Source comment
Basic lemmas connecting total sum to row/col sums

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, Eq, Imo1971P6.totalSum, Finset.sum, Finset.univ, Imo1971P6.rowSum
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
```
lemma totalSum_eq_rowSum_sum : totalSum A = ∑ i, rowSum A i := rfl
```
Mentions: Imo1971P6.totalSum, Imo1971P6.rowSum
lemma Imo1971P6.totalSum_eq_colSum_sum line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, Eq, Imo1971P6.totalSum, Finset.sum, Finset.univ, Imo1971P6.colSum
Proof uses: Finset.sum_comm
4 instances, coercions and auxiliary constants left out.
theorem Imo1971P6.totalSum_transpose_eq line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, Eq, Imo1971P6.totalSum, Matrix.transpose
Proof uses: id, Finset.sum_comm, Finset.univ
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1971P6.aux Auxiliary lemma: The inequality holds if there exists a row with sum x such that x is less than or equal to all row sums and column sums line 51 source
Source documentation
Auxiliary lemma: The inequality holds if there exists a row with sum x such that x is less than or equal to all row sums and column sums.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, LT.lt, OfNat.ofNat, Eq, GE.ge, HAdd.hAdd, Imo1971P6.rowSum, Imo1971P6.colSum, LE.le, Exists, HMul.hMul, Imo1971P6.totalSum, HPow.hPow
Proof uses: dite, Trans.trans, Finset.sum, Finset.univ, Imo1971P6.totalSum_eq_rowSum_sum, Finset.sum_le_sum, Membership.mem, Finset, of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, Finset.card, Finset.sum_const, Fintype.card_fin, eq_self, Eq.mpr, Int and 103 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma aux {n : ℕ} (A : Matrix (Fin n) (Fin n) ℕ) (n_pos : 0 < n)
    (h_cond : ∀ i j : Fin n, A i j = 0 → rowSum A i + colSum A j ≥ n)
    (x : ℕ)
    (h_min_row : ∀ i, x ≤ rowSum A i)
    (h_min_col : ∀ j, x ≤ colSum A j)
    (h_exists_row : ∃ i, rowSum A i = x) :
    2 * totalSum A ≥ n^2 := by
…
```
Mentions: Imo1971P6.rowSum, Imo1971P6.colSum, Imo1971P6.totalSum
problem Imo1971P6.imo1971_p6 line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, LT.lt, OfNat.ofNat, Eq, GE.ge, HAdd.hAdd, Imo1971P6.rowSum, Imo1971P6.colSum, HMul.hMul, Imo1971P6.totalSum, HPow.hPow
Proof uses: Finset, Union.union, Finset.image, Finset.univ, Finset.Nonempty, Exists.intro, Membership.mem, Fin.mk, of_eq_true, Eq.trans, Or, True, Exists, congr, congrArg, And, funext, congrFun', true_and, true_or and 13 more
40 instances, coercions and auxiliary constants left out.

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