Open questions regarding the existence of Euler bricks

References:

• Wikipedia
• stackexchange

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 : (∃ (a : ℕ+) (b : ℕ+) (c : ℕ+), IsPerfectCuboid a b c) ↔ sorry

Is there a perfect Euler brick?

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

Is there an Euler brick in 4-dimensional space?

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

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