`Compfiles/Imo1976P5.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 1976, Problem 5

n is a positive integer and m = 2n. aᵢⱼ = 0, 1 or -1 for 1 ≤ i ≤ n, 1 ≤ j ≤ m. The m unknowns x₁, x₂, ... , xₘ satisfy the n equations:

aᵢ₁x₁ + aᵢ₂x₂ + ... + aᵢₘxₘ = 0,

for i = 1, 2, ... , n. Prove that the system has a solution in integers of absolute value at most m, not all zero.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo1976P5.valueFinset The candidate values for the tuple of unknowns: integers between -n and n in each coordinate line 38 source
Source documentation
The candidate values for the tuple of unknowns: integers between -n and n in each coordinate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, HMul.hMul, OfNat.ofNat, Int
Proof uses: Fintype.piFinset, Finset.Icc, Neg.neg
13 instances, coercions and auxiliary constants left out.
```
noncomputable def valueFinset (n : ℕ) : Finset (Fin (2 * n) → ℤ) :=
…
```
def Imo1976P5.lhsFinset The possible values of the tuple of left-hand sides: each coordinate is an integer between -2n² and 2n² line 43 source
Source documentation
The possible values of the tuple of left-hand sides: each coordinate is an integer between -2n² and 2n².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Int
Proof uses: Fintype.piFinset, Finset.Icc, Neg.neg, HMul.hMul, OfNat.ofNat, HPow.hPow
15 instances, coercions and auxiliary constants left out.
```
noncomputable def lhsFinset (n : ℕ) : Finset (Fin n → ℤ) :=
…
```
def Imo1976P5.lhs The tuple of left-hand sides of the equations, as a function of the tuple of unknowns line 48 source
Source documentation
The tuple of left-hand sides of the equations, as a function of the tuple of unknowns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Int
Proof uses: Finset.sum, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
def lhs (n : ℕ) (a : Fin n → Fin (2 * n) → ℤ) (x : Fin (2 * n) → ℤ) :
    Fin n → ℤ :=
…
```
theorem Imo1976P5.card_valueFinset line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Fin, HMul.hMul, OfNat.ofNat, Int, Imo1976P5.valueFinset, HPow.hPow, HAdd.hAdd
Proof uses: Finset.Icc, Neg.neg, Eq.mpr, Int.toNat, HSub.hSub, id, congrArg, Int.card_Icc, Eq.trans, Nat.cast_add, congr, Nat.cast_mul, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Mathlib.Tactic.Ring.Common.sub_congr, Int.rawCast and 53 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P5.card_lhsFinset line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Fin, Int, Imo1976P5.lhsFinset, HPow.hPow, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Finset.Icc, Neg.neg, Eq.mpr, Int.toNat, HSub.hSub, id, congrArg, Int.card_Icc, Eq.trans, Nat.cast_add, congr, Nat.cast_mul, Nat.cast_pow, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Mathlib.Tactic.Ring.Common.sub_congr and 62 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P5.card_lhs_lt_card_value The pigeonhole step: there are more candidate tuples than possible values of the left-hand sides line 74 source
Source documentation
The pigeonhole step: there are more candidate tuples than possible values of the left-hand sides.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset.card, Fin, Int, Imo1976P5.lhsFinset, HMul.hMul, Imo1976P5.valueFinset
Proof uses: Eq.mpr, HPow.hPow, HAdd.hAdd, id, Eq, congrArg, Imo1976P5.card_lhsFinset, Imo1976P5.card_valueFinset, Eq.symm, pow_mul, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 30 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem card_lhs_lt_card_value (n : ℕ) (hn : 0 < n) :
    (lhsFinset n).card < (valueFinset n).card := by
…
```
Mentions: Imo1976P5.lhsFinset, Imo1976P5.valueFinset
theorem Imo1976P5.mapsTo Each left-hand side is bounded by 2n² when every |xⱼ| ≤ n line 84 source
Source documentation
Each left-hand side is bounded by 2n² when every |xⱼ| ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Int, Or, Eq, Neg.neg, Set.MapsTo, Imo1976P5.lhs, Finset, Imo1976P5.valueFinset, Imo1976P5.lhsFinset
Proof uses: Membership.mem, Set, Eq.mpr, Finset.Icc, HPow.hPow, id, Eq.trans, Fintype.piFinset, LE.le, abs, And, Trans.trans, Finset.sum, Finset.univ, Finset.abs_sum_le_sum_abs, Finset.sum_le_sum, congrArg, abs_mul, of_eq_true, True and 50 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem mapsTo (n : ℕ) (a : Fin n → Fin (2 * n) → ℤ)
    (ha : ∀ i j, a i j = 0 ∨ a i j = 1 ∨ a i j = -1) :
    Set.MapsTo (lhs n a) ↑(valueFinset n) ↑(lhsFinset n) := by
…
```
Mentions: Imo1976P5.lhs, Imo1976P5.valueFinset, Imo1976P5.lhsFinset
problem Imo1976P5.imo1976_p5 line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, HMul.hMul, Int, Or, Eq, Neg.neg, Exists, And, LE.le, abs, Ne, Finset.sum, Finset.univ
Proof uses: Membership.mem, Finset, Imo1976P5.valueFinset, Imo1976P5.lhs, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Imo1976P5.lhsFinset, Imo1976P5.card_lhs_lt_card_value, Imo1976P5.mapsTo, Finset.Icc, Iff.mp, Fintype.piFinset, Fintype.mem_piFinset, Exists.intro, HSub.hSub, And.intro, Eq.mpr, id, congrArg, Pi.sub_apply, propext and 67 more
103 instances, coercions and auxiliary constants left out.

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