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

35 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1976, Problem 3

A rectangular box can be completely filled with unit cubes. If one places as many cubes as possible, each with volume 2, in the box, with their edges parallel to the edges of the box, one can fill exactly 40% of the box. Determine the possible dimensions of the box.

Formalization

The box has integer dimensions a ≤ b ≤ c. A cube of volume 2 has side length k = ∛2 (the real cube root of two). A placement of such cubes in the box, with edges parallel to the edges of the box, is formalized as a finite set P of corner positions satisfying IsPacking a b c P: every cube lies inside the box and distinct cubes have disjoint interiors (NonOverlapping).

The maximal number of cubes that fit is maxNumCubes a b c = ⌊a / k⌋₊ * ⌊b / k⌋₊ * ⌊c / k⌋₊: along an edge of integer length n exactly ⌊n / k⌋₊ cubes fit. The maximality is proved formally rather than asserted: packing_card_le shows that no packing has more cubes (the map sending a cube at (x, y, z) to the triple (⌊x / k⌋₊, ⌊y / k⌋₊, ⌊z / k⌋₊) is injective on a packing), and exists_packing shows that the grid arrangement attains the bound.

The "exactly 40%" condition is stated explicitly as 2 * P.card = 40 / 100 * (a * b * c) for a maximal packing P: the total volume of the cubes is 40% of the box volume. Since a maximal packing has P.card = maxNumCubes a b c, this is equivalent to a * b * c = 5 * (⌊a / k⌋₊ * ⌊b / k⌋₊ * ⌊c / k⌋₊), which is the form used by the integer-arithmetic core of the proof.

Imports (4)

Imported by 1 file

Compfiles.lean

def Imo1976P3.k The side length of a cube of volume 2: the real cube root of 2 line 53 source
Source documentation
The side length of a cube of volume 2: the real cube root of 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HPow.hPow, OfNat.ofNat, Inv.inv
7 instances, coercions and auxiliary constants left out.
```
noncomputable def k : ℝ := (2 : ℝ) ^ (3 : ℝ)⁻¹
```
abbrev Imo1976P3.CubeInBox Documented declaration: CubeInBox line 58 source
Source documentation
A placement of a cube of side k in the a × b × c box: the cube is the closed box [p.1, p.1 + k] × [p.2.1, p.2.1 + k] × [p.2.2, p.2.2 + k], and it must be contained in [0, a] × [0, b] × [0, c].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Real
Proof uses: And, LE.le, OfNat.ofNat, Prod.fst, HAdd.hAdd, Imo1976P3.k, Prod.snd
7 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev CubeInBox (a b c : ℕ) (p : ℝ × ℝ × ℝ) : Prop :=
…
```
abbrev Imo1976P3.NonOverlapping Two cubes of side k placed at p and q do not overlap: their interiors are disjoint, i.e. they are separated along at least one axis line 63 source
Source documentation
Two cubes of side k placed at p and q do not overlap: their interiors are disjoint, i.e. they are separated along at least one axis.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Real
Proof uses: Or, LE.le, HAdd.hAdd, Prod.fst, Imo1976P3.k, Prod.snd
3 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev NonOverlapping (p q : ℝ × ℝ × ℝ) : Prop :=
…
```
structure Imo1976P3.IsPacking Documented declaration: IsPacking line 71 source
Source documentation
A packing of the a × b × c box by cubes of volume 2 (side k = ∛2), with edges parallel to the edges of the box: a finite set of cube positions inside the box, pairwise non-overlapping.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Real
```
structure IsPacking (a b c : ℕ) (P : Finset (ℝ × ℝ × ℝ)) : Prop where
…
```
Mentions: P
def Imo1976P3.maxNumCubes Documented declaration: maxNumCubes line 80 source
Source documentation
The maximal number of cubes of volume 2 that can be placed in the a × b × c box with edges parallel to the edges of the box: along an edge of integer length n exactly ⌊n / k⌋₊ cubes fit. That this is indeed the maximum is proved in packing_card_le (upper bound) and exists_packing (the grid arrangement attains it).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HMul.hMul, Nat.floor, Real, HDiv.hDiv, Imo1976P3.k
13 instances, coercions and auxiliary constants left out.
```
noncomputable def maxNumCubes (a b c : ℕ) : ℕ :=
…
```
theorem Imo1976P3.k_pos line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, OfNat.ofNat, Imo1976P3.k
Proof uses: Real.rpow_pos_of_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, Inv.inv
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.k_cube line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, HPow.hPow, Nat, Imo1976P3.k, OfNat.ofNat
Proof uses: Real.rpow_inv_natCast_pow, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.IsNat.raw_refl, Bool.false
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.one_lt_k line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, OfNat.ofNat, Imo1976P3.k
Proof uses: Decidable.byContradiction, Not, LE.le, HPow.hPow, Nat, pow_le_pow_left₀, LT.lt.le, Imo1976P3.k_pos, Eq.mp, False.elim, False, eq_false, Mathlib.Meta.NormNum.isNat_le_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_pow, Nat.cast_one, Mathlib.Meta.NormNum.one_natPow, Bool and 3 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.k_lt_two line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, Imo1976P3.k, OfNat.ofNat, Nat
Proof uses: Decidable.byContradiction, Not, LE.le, HPow.hPow, pow_le_pow_left₀, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, Eq.mp, False.elim, False, eq_false, Mathlib.Meta.NormNum.isNat_le_false, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1 and 3 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.floor_div_k_mul_le The number of cubes that fit along an edge of integer length n, times the cube side, is at most the edge length line 107 source
Source documentation
The number of cubes that fit along an edge of integer length n, times the cube side, is at most the edge length.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, HMul.hMul, Nat.floor, HDiv.hDiv, Imo1976P3.k
Proof uses: Nat.floor_le, div_nonneg, Nat.cast_nonneg, LT.lt.le, OfNat.ofNat, Imo1976P3.k_pos, Trans.trans, Eq, mul_le_mul_of_nonneg_right, div_mul_cancel₀, LT.lt.ne'
45 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem floor_div_k_mul_le (n : ℕ) : (⌊(n : ℝ) / k⌋₊ : ℝ) * k ≤ n := by
…
```
Mentions: Imo1976P3.k
theorem Imo1976P3.fin_cast_k_add_k_le A cube whose left face is at i * k with i < ⌊n / k⌋₊ lies within an edge of integer length n line 116 source
Source documentation
A cube whose left face is at i * k with i < ⌊n / k⌋₊ lies within an edge of integer length n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Nat.floor, Real, HDiv.hDiv, Imo1976P3.k, LE.le, HAdd.hAdd, HMul.hMul
Proof uses: OfNat.ofNat, Fin.isLt, mul_le_mul_of_nonneg_right, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, LT.lt.le, Imo1976P3.k_pos, Trans.trans, Eq, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 19 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem fin_cast_k_add_k_le {n : ℕ} (i : Fin ⌊(n : ℝ) / k⌋₊) :
    (i.1 : ℝ) * k + k ≤ n := by
…
```
Mentions: Imo1976P3.k
theorem Imo1976P3.floor_lt_floor_of_add_k_le A cube inside an edge of integer length n, with left face at x, has ⌊x / k⌋₊ < ⌊n / k⌋₊ line 127 source
Source documentation
A cube inside an edge of integer length n, with left face at x, has ⌊x / k⌋₊ < ⌊n / k⌋₊.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LE.le, OfNat.ofNat, HAdd.hAdd, Imo1976P3.k, LT.lt, Nat.floor, HDiv.hDiv
Proof uses: Nat.floor_le, div_nonneg, LT.lt.le, Imo1976P3.k_pos, mul_le_mul_of_nonneg_right, Inv.inv, Iff.mpr, inv_nonneg, Eq.mpr, id, Eq, congrArg, add_div, div_self, LT.lt.ne', Eq.refl, Nat.lt_floor_add_one, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 68 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem floor_lt_floor_of_add_k_le {n : ℕ} {x : ℝ} (hx0 : 0 ≤ x) (hxn : x + k ≤ n) :
    ⌊x / k⌋₊ < ⌊(n : ℝ) / k⌋₊ := by
…
```
Mentions: Imo1976P3.k
theorem Imo1976P3.sub_lt_k_of_floor_eq Two positions with the same integer part of x / k differ by less than k line 141 source
Source documentation
Two positions with the same integer part of x / k differ by less than k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Eq, Nat, Nat.floor, HDiv.hDiv, Imo1976P3.k, And, LT.lt, HSub.hSub
Proof uses: HAdd.hAdd, Nat.lt_floor_add_one, Nat.floor_le, div_nonneg, LT.lt.le, Imo1976P3.k_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast and 63 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem sub_lt_k_of_floor_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y)
    (h : ⌊x / k⌋₊ = ⌊y / k⌋₊) : x - y < k ∧ y - x < k := by
…
```
Mentions: h, Imo1976P3.k
def Imo1976P3.cubeCode The code of a cube position: the integer parts of its coordinates divided by k line 163 source
Source documentation
The code of a cube position: the integer parts of its coordinates divided by k. Two positions sharing all three codes have left faces strictly within k of each other along every axis, so their interiors overlap; hence the code is injective on any packing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Real, Nat
Proof uses: Prod.mk, Nat.floor, HDiv.hDiv, Prod.fst, Imo1976P3.k, Prod.snd
9 instances, coercions and auxiliary constants left out.
```
noncomputable def cubeCode (p : ℝ × ℝ × ℝ) : ℕ × ℕ × ℕ :=
…
```
theorem Imo1976P3.packing_card_le The upper bound half of the maximal condition: no packing of the a × b × c box has more than maxNumCubes a b c cubes line 168 source
Source documentation
The upper bound half of the maximal condition: no packing of the a × b × c box has more than maxNumCubes a b c cubes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Real, Imo1976P3.IsPacking, LE.le, Finset.card, Imo1976P3.maxNumCubes
Proof uses: Set.MapsTo, Imo1976P3.cubeCode, SProd.sprod, Finset.range, Nat.floor, HDiv.hDiv, Imo1976P3.k, Membership.mem, Set, Imo1976P3.CubeInBox, Imo1976P3.IsPacking.inBox, Iff.mp, Finset.mem_coe, Iff.mpr, And, Prod.fst, Prod.snd, Finset.mem_product, And.intro, LT.lt and 72 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
theorem packing_card_le (a b c : ℕ) (P : Finset (ℝ × ℝ × ℝ)) (hP : IsPacking a b c P) :
    P.card ≤ maxNumCubes a b c := by
…
```
Mentions: P, Imo1976P3.IsPacking, Imo1976P3.maxNumCubes
abbrev Imo1976P3.gridPos The grid arrangement of cube positions: cubes at (i * k, j * k, l * k) for i < ⌊a / k⌋₊, j < ⌊b / k⌋₊, l < ⌊c / k⌋₊ line 210 source
Source documentation
The grid arrangement of cube positions: cubes at (i * k, j * k, l * k) for i < ⌊a / k⌋₊, j < ⌊b / k⌋₊, l < ⌊c / k⌋₊.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Fin, Nat.floor, Real, HDiv.hDiv, Imo1976P3.k
Proof uses: Prod.mk, HMul.hMul, Prod.fst, Prod.snd
25 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev gridPos {a b c : ℕ}
    (t : Fin ⌊(a : ℝ) / k⌋₊ × Fin ⌊(b : ℝ) / k⌋₊ × Fin ⌊(c : ℝ) / k⌋₊) : ℝ × ℝ × ℝ :=
…
```
Mentions: Imo1976P3.k
theorem Imo1976P3.grid_inj line 214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Injective, Prod, Fin, Nat.floor, Real, HDiv.hDiv, Imo1976P3.k, Imo1976P3.gridPos
Proof uses: Eq, HMul.hMul, Prod.fst, And, Prod.snd, Eq.mp, Eq.trans, Prod.mk, Prod.mk.injEq, congrArg, mul_right_cancel₀, LT.lt.ne', OfNat.ofNat, Imo1976P3.k_pos, cast, Iff.mpr, Prod.ext_iff, And.intro, Fin.ext_iff
38 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.separated_of_ne Two distinct grid indices give cubes separated along that axis line 231 source
Source documentation
Two distinct grid indices give cubes separated along that axis.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, Or, LE.le, Real, HAdd.hAdd, HMul.hMul, Imo1976P3.k
Proof uses: LT.lt, lt_or_gt_of_ne, Or.inl, OfNat.ofNat, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, mul_le_mul_of_nonneg_right, LT.lt.le, Imo1976P3.k_pos, Trans.trans, Eq, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr and 21 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem separated_of_ne {i j : ℕ} (h : i ≠ j) :
    (i : ℝ) * k + k ≤ (j : ℝ) * k ∨ (j : ℝ) * k + k ≤ (i : ℝ) * k := by
…
```
Mentions: h, Imo1976P3.k
theorem Imo1976P3.exists_packing The attainment half of the maximal condition: the grid arrangement is a packing with exactly maxNumCubes a b c cubes line 247 source
Source documentation
The attainment half of the maximal condition: the grid arrangement is a packing with exactly maxNumCubes a b c cubes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, Prod, Real, And, Imo1976P3.IsPacking, Eq, Finset.card, Imo1976P3.maxNumCubes
Proof uses: Exists.intro, Finset.image, Fin, Nat.floor, HDiv.hDiv, Imo1976P3.k, Imo1976P3.gridPos, Finset.univ, And.intro, Imo1976P3.IsPacking.mk, Membership.mem, Imo1976P3.CubeInBox, Iff.mp, Finset.mem_image, LE.le, OfNat.ofNat, Prod.fst, HAdd.hAdd, Prod.snd, mul_nonneg and 33 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
theorem exists_packing (a b c : ℕ) :
    ∃ P : Finset (ℝ × ℝ × ℝ), IsPacking a b c P ∧ P.card = maxNumCubes a b c := by
…
```
Mentions: P, Imo1976P3.IsPacking, Imo1976P3.maxNumCubes
theorem Imo1976P3.floor_spec The defining property of ⌊n / k⌋₊, expressed with integers only: 2 * n'^3 ≤ n^3 < 2 * (n' + 1)^3, obtained by cubing n' * k ≤ n < (n' + 1) * k line 280 source
Source documentation
The defining property of ⌊n / k⌋₊, expressed with integers only: 2 * n'^3 ≤ n^3 < 2 * (n' + 1)^3, obtained by cubing n' * k ≤ n < (n' + 1) * k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow, Nat.floor, Real, HDiv.hDiv, Imo1976P3.k, LT.lt, HAdd.hAdd
Proof uses: Nat.floor_le, div_nonneg, Nat.cast_nonneg, LT.lt.le, Imo1976P3.k_pos, Nat.lt_floor_add_one, Iff.mp, le_div_iff₀, div_lt_iff₀, pow_le_pow_left₀, mul_nonneg, pow_lt_pow_left₀, three_ne_zero, And.intro, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, inferInstance, AddMonoidWithOne and 86 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem floor_spec (n : ℕ) :
    2 * ⌊(n : ℝ) / k⌋₊ ^ 3 ≤ n ^ 3 ∧ n ^ 3 < 2 * (⌊(n : ℝ) / k⌋₊ + 1) ^ 3 := by
…
```
Mentions: Imo1976P3.k
theorem Imo1976P3.le_of_cube_le Comparing x * k with an integer by comparing cubes line 302 source
Source documentation
Comparing x * k with an integer by comparing cubes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, LE.le, HPow.hPow, HMul.hMul, Imo1976P3.k, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, LT.lt, pow_lt_pow_left₀, Eq.mp, Nat.cast_nonneg, three_ne_zero, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 51 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem le_of_cube_le {x : ℝ} (n : ℕ) (h : (x * k) ^ 3 ≤ (n : ℝ) ^ 3) : x * k ≤ (n : ℝ) := by
…
```
Mentions: h, Imo1976P3.k
theorem Imo1976P3.lt_of_cube_lt Comparing an integer with x * k by comparing cubes line 309 source
Source documentation
Comparing an integer with x * k by comparing cubes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Nat, LT.lt, HPow.hPow, HMul.hMul, Imo1976P3.k
Proof uses: Decidable.byContradiction, Not, pow_le_pow_left₀, mul_nonneg, LT.lt.le, Imo1976P3.k_pos, Eq.mp, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 51 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem lt_of_cube_lt {x : ℝ} (hx : 0 ≤ x) (n : ℕ) (h : (n : ℝ) ^ 3 < (x * k) ^ 3) :
    (n : ℝ) < x * k := by
…
```
Mentions: h, Imo1976P3.k
theorem Imo1976P3.floor_val Evaluating ⌊n / k⌋₊ from the two inequalities c * k ≤ n < (c + 1) * k line 317 source
Source documentation
Evaluating ⌊n / k⌋₊ from the two inequalities c * k ≤ n < (c + 1) * k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, HMul.hMul, Imo1976P3.k, LT.lt, HAdd.hAdd, OfNat.ofNat, Eq, Nat.floor, HDiv.hDiv
Proof uses: Iff.mpr, And, Nat.floor_eq_iff, div_nonneg, Nat.cast_nonneg, LT.lt.le, Imo1976P3.k_pos, And.intro, le_div_iff₀, div_lt_iff₀
73 instances, coercions and auxiliary constants left out.
```
theorem floor_val (n c : ℕ) (h1 : (c : ℝ) * k ≤ (n : ℝ)) (h2 : (n : ℝ) < ((c : ℝ) + 1) * k) :
    ⌊(n : ℝ) / k⌋₊ = c :=
…
```
Mentions: Imo1976P3.k
theorem Imo1976P3.floor_two line 322 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.floor, Real, HDiv.hDiv, OfNat.ofNat, Imo1976P3.k
Proof uses: Imo1976P3.floor_val, Eq.mpr, LE.le, HMul.hMul, id, congrArg, Nat.cast_one, one_mul, LT.lt.le, Imo1976P3.k_lt_two, LT.lt, HAdd.hAdd, congrFun', lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 54 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.floor_three line 329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.floor, Real, HDiv.hDiv, OfNat.ofNat, Imo1976P3.k
Proof uses: Imo1976P3.floor_val, Imo1976P3.le_of_cube_le, Eq.mpr, LE.le, HPow.hPow, HMul.hMul, id, congrArg, mul_pow, Imo1976P3.k_cube, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, Mathlib.Meta.NormNum.instAtLeastTwo, Bool and 59 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.floor_five line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.floor, Real, HDiv.hDiv, OfNat.ofNat, Imo1976P3.k
Proof uses: Imo1976P3.floor_val, Imo1976P3.le_of_cube_le, Eq.mpr, LE.le, HPow.hPow, HMul.hMul, id, congrArg, mul_pow, Imo1976P3.k_cube, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, Mathlib.Meta.NormNum.instAtLeastTwo, Bool and 9 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.floor_six line 348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.floor, Real, HDiv.hDiv, OfNat.ofNat, Imo1976P3.k
Proof uses: Imo1976P3.floor_val, Imo1976P3.le_of_cube_le, Eq.mpr, LE.le, HPow.hPow, HMul.hMul, id, congrArg, mul_pow, Imo1976P3.k_cube, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, Mathlib.Meta.NormNum.instAtLeastTwo, Bool and 9 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo1976P3.det_of From here on everything is integer arithmetic line 361 source
Source documentation
From here on everything is integer arithmetic. det_of pins down n' once n is known concretely.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow, LT.lt, HAdd.hAdd, Eq
Proof uses: Decidable.byContradiction, Not, Nat.pow_le_pow_left, Nat.succ, Eq.mp, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Int, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr and 71 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem det_of {n x c : ℕ} (hc1 : 2 * c ^ 3 ≤ n ^ 3) (hc2 : n ^ 3 < 2 * (c + 1) ^ 3)
    (h1 : 2 * x ^ 3 ≤ n ^ 3) (h2 : n ^ 3 < 2 * (x + 1) ^ 3) : x = c := by
…
```
theorem Imo1976P3.two_le_of If 1 ≤ n' and 2 * n'^3 ≤ n^3 then 2 ≤ n line 376 source
Source documentation
If 1 ≤ n' and 2 * n'^3 ≤ n^3 then 2 ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow
Proof uses: Trans.trans, Eq, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.one_natPow, mul_le_mul_right, Nat.pow_le_pow_left, Decidable.byContradiction, Not, dite, False, LT.lt, False.elim, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_le_false, Bool and 9 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem two_le_of {n n' : ℕ} (hn' : 1 ≤ n') (h1 : 2 * n' ^ 3 ≤ n ^ 3) : 2 ≤ n := by
…
```
theorem Imo1976P3.five_cubed The key ratio bound: for n ≥ 3, n^3 < 5 * n'^3 line 386 source
Source documentation
The key ratio bound: for n ≥ 3, n^3 < 5 * n'^3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, LT.lt, HAdd.hAdd
Proof uses: GE.ge, Or, Nat.lt_or_ge, dite, Eq, Imo1976P3.det_of, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_add, Bool.false, Eq.symm, le_antisymm and 92 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
theorem five_cubed {n n' : ℕ} (hn : 3 ≤ n) (h1 : 2 * n' ^ 3 ≤ n ^ 3)
    (h2 : n ^ 3 < 2 * (n' + 1) ^ 3) : n ^ 3 < 5 * n' ^ 3 := by
…
```
theorem Imo1976P3.key500 Auxiliary estimate: 343 * (m + 1)^3 ≤ 500 * m^3 for m ≥ 8 line 423 source
Source documentation
Auxiliary estimate: 343 * (m + 1)^3 ≤ 500 * m^3 for m ≥ 8.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, HAdd.hAdd
Proof uses: Eq, Exists, Exists.intro, HSub.hSub, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr and 76 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem key500 {m : ℕ} (hm : 8 ≤ m) : 343 * (m + 1) ^ 3 ≤ 500 * m ^ 3 := by
…
```
theorem Imo1976P3.seven_lt_ten The second ratio bound: for n ≥ 11, 7 * n < 10 * n' line 428 source
Source documentation
The second ratio bound: for n ≥ 11, 7 * n < 10 * n'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, LT.lt, HAdd.hAdd
Proof uses: Decidable.byContradiction, Not, Nat.pow_le_pow_left, Eq.mp, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Int, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 78 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem seven_lt_ten {n n' : ℕ} (hn : 11 ≤ n) (_h1 : 2 * n' ^ 3 ≤ n ^ 3)
    (h2 : n ^ 3 < 2 * (n' + 1) ^ 3) : 7 * n < 10 * n' := by
…
```
theorem Imo1976P3.main_nat The integer core of the problem: the only sorted triples satisfying the volume equation are (2, 3, 5) and (2, 5, 6) line 444 source
Source documentation
The integer core of the problem: the only sorted triples satisfying the volume equation are (2, 3, 5) and (2, 5, 6).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HPow.hPow, HAdd.hAdd, Eq, Or, And
Proof uses: mul_pos, Decidable.byContradiction, Not, False, False.elim, Eq.mp, Eq.trans, congrArg, congrFun', MulZeroClass.zero_mul, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.zero_le, MulZeroClass.mul_zero and 117 more
152 instances, coercions and auxiliary constants left out.

Tactic trace: 250 steps (first 200 of 250)
Open to load the checked before-and-after goal states.
```
theorem main_nat {a b c a' b' c' : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (hab : a ≤ b) (hbc : b ≤ c)
    (ha1 : 2 * a' ^ 3 ≤ a ^ 3) (ha2 : a ^ 3 < 2 * (a' + 1) ^ 3)
    (hb1 : 2 * b' ^ 3 ≤ b ^ 3) (hb2 : b ^ 3 < 2 * (b' + 1) ^ 3)
    (hc1 : 2 * c' ^ 3 ≤ c ^ 3) (hc2 : c ^ 3 < 2 * (c' + 1) ^ 3)
    (h : a * b * c = 5 * (a' * b' * c')) :
    (a = 2 ∧ b = 3 ∧ c = 5) ∨ (a = 2 ∧ b = 5 ∧ c = 6) := by
…
```
Mentions: h
determine Imo1976P3.solution_set line 634 source
no axioms what this means
Statement uses: Set, Prod, Nat
Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton
3 instances, coercions and auxiliary constants left out.
problem Imo1976P3.imo1976_p3 line 636 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Iff, Membership.mem, Prod, Set, Imo1976P3.solution_set, Prod.mk, Exists, Finset, Real, And, Imo1976P3.IsPacking, Finset.card, Eq, HMul.hMul, HDiv.hDiv
Proof uses: Iff.intro, Or, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congr, congrArg, Prod.mk.injEq, Imo1976P3.maxNumCubes, Imo1976P3.exists_packing, Exists.intro, And.intro, Eq.mpr, id, Imo1976P3.packing_card_le, of_eq_true, True, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.instAddMonoidWithOne' and 104 more
124 instances, coercions and auxiliary constants left out.

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