EulerBrick.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 10 curated AI-written annotations and 7190 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 project documentation, Formal Conjectures paper, arXiv v1

16 declarations, 7 contain sorry, 0 declared as axioms

Open questions regarding the existence of Euler bricks

References:

Wikipedia
stackexchange
[Sh12] Sharipov, Ruslan. Perfect cuboids and irreducible polynomials. https://arxiv.org/abs/1108.5348

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

def EulerBrick.IsEulerBrick An Euler brick is a rectangular cuboid where all edges and face diagonals have integer lengths line 36 source
Source documentation
An Euler brick is a rectangular cuboid where all edges and face diagonals have integer lengths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat
Proof uses: And, IsSquare, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
def IsEulerBrick (a b c : ℕ+) : Prop :=
…
```
Mentions: c
def EulerBrick.IsPerfectCuboid A perfect cuboid is an Euler brick with an integer space diagonal line 42 source
Source documentation
A perfect cuboid is an Euler brick with an integer space diagonal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat
Proof uses: And, EulerBrick.IsEulerBrick, IsSquare, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
def IsPerfectCuboid (a b c : ℕ+) : Prop :=
…
```
Mentions: c
def EulerBrick.IsEulerHyperBrick Generalization of an Euler brick to $n$-dimensional space line 48 source
Source documentation
Generalization of an Euler brick to $n$-dimensional space.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, PNat
Proof uses: Pairwise, IsSquare, HAdd.hAdd, HPow.hPow, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
def IsEulerHyperBrick (n : ℕ) (sides : Fin n → ℕ+) : Prop :=
…
```
theorem EulerBrick.perfect_euler_brick_existence Is there a perfect Euler brick? sorry line 55 source
Source documentation
Is there a perfect Euler brick?

depends on sorry what this means
Statement uses: Iff, True, Exists, PNat, EulerBrick.IsPerfectCuboid
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem perfect_euler_brick_existence :
    answer(sorry) ↔ ∃ a b c : ℕ+, IsPerfectCuboid a b c := by
…
```
Mentions: c, EulerBrick.IsPerfectCuboid
theorem EulerBrick.four_dim_euler_brick_existence Is there an Euler brick in $4$-dimensional space? sorry line 63 source
Source documentation
Is there an Euler brick in $4$-dimensional space?

depends on sorry what this means
Statement uses: Iff, True, Exists, Fin, OfNat.ofNat, Nat, PNat, EulerBrick.IsEulerHyperBrick
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem four_dim_euler_brick_existence :
    answer(sorry) ↔ ∃ sides : Fin 4 → ℕ+, IsEulerHyperBrick 4 sides:= by
…
```
Mentions: EulerBrick.IsEulerHyperBrick
theorem EulerBrick.n_dim_euler_brick_existence Is there an Euler brick in $n$-dimensional space for any $n > 3$? sorry line 71 source
Source documentation
Is there an Euler brick in $n$-dimensional space for any $n > 3$?

depends on sorry what this means
Statement uses: Iff, True, Nat, GT.gt, OfNat.ofNat, Exists, Fin, PNat, EulerBrick.IsEulerHyperBrick
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem n_dim_euler_brick_existence :
answer(sorry) ↔ ∀ n > 3, ∃ sides : Fin n → ℕ+, IsEulerHyperBrick n sides := by
…
```
Mentions: EulerBrick.IsEulerHyperBrick
def EulerBrick.CuboidOneFor Pairs of natural numbers for which the first Cuboid polynomial is irreducible line 85 source
Source documentation
Pairs of natural numbers for which the first Cuboid polynomial is irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int
Proof uses: Irreducible, Polynomial, HAdd.hAdd, HSub.hSub, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, HMul.hMul, RingHom, Polynomial.C
22 instances, coercions and auxiliary constants left out.
```
def CuboidOneFor (a b : ℤ) : Prop :=
…
```
def EulerBrick.CuboidOne First Cuboid conjecture*: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the first Cuboid polynomial is irreducible line 92 source
Source documentation
First Cuboid conjecture: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the first Cuboid polynomial is irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Int, Eq, GCDMonoid.gcd, OfNat.ofNat, LT.lt, Ne, EulerBrick.CuboidOneFor
5 instances, coercions and auxiliary constants left out.
```
def CuboidOne : Prop := ∀ ⦃a b : ℤ⦄, gcd a b = 1 → 0 < a → 0 < b → a ≠ b → CuboidOneFor a b
…
```
Mentions: EulerBrick.CuboidOneFor
theorem EulerBrick.cuboidOne sorry line 105 source
depends on sorry what this means
Statement uses: EulerBrick.CuboidOne
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def EulerBrick.CuboidTwoFor Pairs of natural numbers for which the second Cuboid polynomial is irreducible line 109 source
Source documentation
Pairs of natural numbers for which the second Cuboid polynomial is irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int
Proof uses: Irreducible, Polynomial, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, HMul.hMul, RingHom, Polynomial.C, Neg.neg
23 instances, coercions and auxiliary constants left out.
```
def CuboidTwoFor (a b : ℤ) : Prop :=
…
```
def EulerBrick.CuboidTwo Second Cuboid conjecture*: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the second Cuboid polynomial is irreducible line 119 source
Source documentation
Second Cuboid conjecture: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the second Cuboid polynomial is irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, Nat.Coprime, LT.lt, OfNat.ofNat, Ne, EulerBrick.CuboidTwoFor, Int
4 instances, coercions and auxiliary constants left out.
```
def CuboidTwo : Prop := ∀ ⦃a b : ℕ⦄, a.Coprime b → 0 < a → 0 < b → a ≠ b → CuboidTwoFor a b
…
```
Mentions: EulerBrick.CuboidTwoFor
theorem EulerBrick.cuboidTwo The second Cuboid conjecture sorry line 123 source
Source documentation
The second Cuboid conjecture

depends on sorry what this means
Statement uses: EulerBrick.CuboidTwo
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cuboidTwo : CuboidTwo := by
…
```
Mentions: EulerBrick.CuboidTwo
def EulerBrick.CuboidThreeFor Triplets of natural numbers for which the third Cuboid polynomial is irreducible line 127 source
Source documentation
Triplets of natural numbers for which the third Cuboid polynomial is irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int
Proof uses: Irreducible, Polynomial, HAdd.hAdd, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, HMul.hMul, RingHom, Polynomial.C, HSub.hSub
20 instances, coercions and auxiliary constants left out.
```
def CuboidThreeFor (a b c : ℤ) : Prop :=
…
```
Mentions: c
def EulerBrick.CuboidThree Third Cuboid conjecture*: For all positive, pairwise different coprime integers line 140 source
Source documentation
Third Cuboid conjecture: For all positive, pairwise different coprime integers $a, b, c$ with $b * c ≠ a ^ 2$ and $a * c ≠ b ^ 2$, the polynomial of the third Cuboid polynomial is irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Int, Eq, GCDMonoid.gcd, OfNat.ofNat, LT.lt, Ne, HMul.hMul, HPow.hPow, Nat, EulerBrick.CuboidThreeFor
12 instances, coercions and auxiliary constants left out.
```
def CuboidThree : Prop := ∀ ⦃a b c : ℤ⦄, gcd a (gcd b c) = 1 → 0 < a → 0 < b →
…
```
Mentions: c
theorem EulerBrick.cuboidThree The third Cuboid conjecture sorry line 145 source
Source documentation
The third Cuboid conjecture

depends on sorry what this means
Statement uses: EulerBrick.CuboidThree
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cuboidThree : CuboidThree := by
…
```
Mentions: EulerBrick.CuboidThree
theorem EulerBrick.cuboid_perfect_euler_brick In [Sh12], Ruslan notes that a perfect Euler brick does not exist if all three Cuboid conjectures hold sorry line 151 source
Source documentation
In [Sh12], Ruslan notes that a perfect Euler brick does not exist if all three Cuboid conjectures hold.

depends on sorry what this means
Statement uses: EulerBrick.CuboidOne, EulerBrick.CuboidTwo, EulerBrick.CuboidThree, Not, Exists, PNat, EulerBrick.IsPerfectCuboid
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cuboid_perfect_euler_brick (h₁ : CuboidOne) (h₂ : CuboidTwo) (h₃ : CuboidThree) :
    ¬ ∃ a b c : ℕ+, IsPerfectCuboid a b c := by
…
```
Mentions: EulerBrick.CuboidOne, EulerBrick.CuboidTwo, EulerBrick.CuboidThree, c, EulerBrick.IsPerfectCuboid