Open questions regarding the existence of Euler bricks

References:

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

def EulerBrick.IsEulerBrick (a b c : ℕ+) : Prop

An Euler brick is a rectangular cuboid where all edges and face diagonals have integer lengths.

Equations

• EulerBrick.IsEulerBrick a b c = (IsSquare (a ^ 2 + b ^ 2) ∧ IsSquare (a ^ 2 + c ^ 2) ∧ IsSquare (b ^ 2 + c ^ 2))

def EulerBrick.IsPerfectCuboid (a b c : ℕ+) : Prop

A perfect cuboid is an Euler brick with an integer space diagonal.

Equations

• EulerBrick.IsPerfectCuboid a b c = (EulerBrick.IsEulerBrick a b c ∧ IsSquare (a ^ 2 + b ^ 2 + c ^ 2))

def EulerBrick.IsEulerHyperBrick (n : ℕ) (sides : Fin n → ℕ+) : Prop

Generalization of an Euler brick to $n$-dimensional space.

Equations

• EulerBrick.IsEulerHyperBrick n sides = Pairwise fun (i j : Fin n) => IsSquare (sides i ^ 2 + sides j ^ 2)

theorem EulerBrick.perfect_euler_brick_existence : sorry ↔ ∃ (a : ℕ+) (b : ℕ+) (c : ℕ+), IsPerfectCuboid a b c

Is there a perfect Euler brick?

theorem EulerBrick.four_dim_euler_brick_existence : sorry ↔ ∃ (sides : Fin 4 → ℕ+), IsEulerHyperBrick 4 sides

Is there an Euler brick in $4$-dimensional space?

theorem EulerBrick.n_dim_euler_brick_existence : sorry ↔ ∀ n > 3, ∃ (sides : Fin n → ℕ+), IsEulerHyperBrick n sides

Is there an Euler brick in $n$-dimensional space for any $n > 3$?

Cuboid conjectures: The three Cuboid conjectures ask if certain families of polynomials are always irreducible. If all hold, this implies the nonexistence of a perfect Euler brick.

def EulerBrick.CuboidOneFor (a b : ℤ) : Prop

Pairs of natural numbers for which the first Cuboid polynomial is irreducible.

Equations

• One or more equations did not get rendered due to their size.

def EulerBrick.CuboidOne : Prop

First Cuboid conjecture: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the first Cuboid polynomial is irreducible.

Equations

• EulerBrick.CuboidOne = ∀ ⦃a b : ℤ⦄, gcd a b = 1 → 0 < a → 0 < b → a ≠ b → EulerBrick.CuboidOneFor a b

theorem EulerBrick.cuboidOne : CuboidOne

The first Cuboid conjecture

def EulerBrick.CuboidTwoFor (a b : ℤ) : Prop

Pairs of natural numbers for which the second Cuboid polynomial is irreducible.

Equations

• One or more equations did not get rendered due to their size.

def EulerBrick.CuboidTwo : Prop

Second Cuboid conjecture: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the second Cuboid polynomial is irreducible.

Equations

• EulerBrick.CuboidTwo = ∀ ⦃a b : ℕ⦄, a.Coprime b → 0 < a → 0 < b → a ≠ b → EulerBrick.CuboidTwoFor ↑a ↑b

theorem EulerBrick.cuboidTwo : CuboidTwo

The second Cuboid conjecture

def EulerBrick.CuboidThreeFor (a b c : ℤ) : Prop

Triplets of natural numbers for which the third Cuboid polynomial is irreducible.

Equations

• One or more equations did not get rendered due to their size.

def EulerBrick.CuboidThree : Prop

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.

Equations

• EulerBrick.CuboidThree = ∀ ⦃a b c : ℤ⦄, gcd a (gcd b c) = 1 → 0 < a → 0 < b → 0 < c → a ≠ b → b ≠ c → c ≠ a → b * c ≠ a ^ 2 → a * c ≠ b ^ 2 → EulerBrick.CuboidThreeFor a b c

theorem EulerBrick.cuboidThree : CuboidThree

The third Cuboid conjecture

theorem EulerBrick.cuboid_perfect_euler_brick (h₁ : CuboidOne) (h₂ : CuboidTwo) (h₃ : CuboidThree) : ¬∃ (a : ℕ+) (b : ℕ+) (c : ℕ+), IsPerfectCuboid a b c

In [Sh12], Ruslan notes that a perfect Euler brick does not exist if all three Cuboid conjectures hold.