FormalConjectures.Wikipedia.EulerBrick

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil

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


namespace EulerBrick

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

def IsEulerBrick (a b c : ℕ+) : Prop :=
  IsSquare (a^2 + b^2) ∧ IsSquare (a^2 + c^2) ∧ IsSquare (b^2 + c^2)

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

def IsPerfectCuboid (a b c : ℕ+) : Prop :=
  IsEulerBrick a b c ∧ IsSquare (a^2 + b^2 + c^2)

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

def IsEulerHyperBrick (n : ℕ) (sides : Fin n → ℕ+) : Prop :=
  Pairwise fun i j ↦ IsSquare ((sides i)^2 + (sides j)^2)

Is there a perfect Euler brick?

@[category research open, AMS 11]
theorem declaration uses 'sorry'perfect_euler_brick_existence :
    answer(sorry) ↔ ∃ a b c : ℕ+, IsPerfectCuboid a b c := by⊢ True ↔ ∃ a b c, IsPerfectCuboid a b c
  sorryAll goals completed! 🐙

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

@[category research open, AMS 11]
theorem declaration uses 'sorry'four_dim_euler_brick_existence :
    answer(sorry) ↔ ∃ sides : Fin 4 → ℕ+, IsEulerHyperBrick 4 sides:= by⊢ True ↔ ∃ sides, IsEulerHyperBrick 4 sides
  sorryAll goals completed! 🐙

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

@[category research open, AMS 11]
theorem declaration uses 'sorry'n_dim_euler_brick_existence :
answer(sorry) ↔ ∀ n > 3, ∃ sides : Fin n → ℕ+, IsEulerHyperBrick n sides := by⊢ True ↔ ∀ n > 3, ∃ sides, IsEulerHyperBrick n sides
  sorryAll goals completed! 🐙


section Cuboid


open Polynomial

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

def CuboidOneFor (a b : ℤ) : Prop :=
  Irreducible (X ^ 8 + C (6 * (a ^ 2 - b ^ 2)) * X ^ 6
    + C (b ^ 4 - 4 * a ^ 2 * b ^ 2 + a ^ 4) * X ^ 4
    - C (6 * a ^ 2 * b ^ 2 * (a ^ 2 - b ^ 2)) * X ^ 2 + C (a ^ 4 * b ^ 4))

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

def CuboidOne : Prop := ∀ ⦃a b : ℤ⦄, gcd a b = 1 → 0 < a → 0 < b → a ≠ b → CuboidOneFor a b

The first Cuboid conjecture

The DeepMind prover agent has found a formal disproof of this statement.

An (independent) informal solution can be found here: Reference: arxiv/2510.11768 Irreducibility of the Cuboid Polynomial P_{a,u}(t) via a Rank-Zero Elliptic Curve by Valery Asiryan

@[category research solved, AMS 12, formal_proof using formal_conjectures at
"https://github.com/google-deepmind/formal-conjectures/blob/34c93bbad127a9a5354b9d53478d338eb65edb88/FormalConjectures/Wikipedia/EulerBrick.lean#L1804"]
theorem declaration uses 'sorry'cuboidOne : CuboidOne := by⊢ CuboidOne
  sorryAll goals completed! 🐙

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

def CuboidTwoFor (a b : ℤ) : Prop :=
  Irreducible (X ^ 10 + C ((2 * b ^ 2 + a ^ 2) * (3 * b ^ 2 - 2 * a ^ 2)) * X ^ 8
    + C ((b ^ 8 + 10 * a ^ 2 * b ^ 6 + 4 * a ^ 4 * b ^ 4 - 14 * a ^ 6 * b ^ 2 + a ^ 8)) * X ^ 6
    - C (a ^ 2 * b ^ 2 * (b ^ 8 - 14 * a ^ 2 * b ^ 6
    + 4 * a ^ 4 * b ^ 4 + 10 * a ^ 6 * b ^ 2 + a ^ 8))
    * X ^ 4 - C (a ^ 6 * b ^ 6 * (b ^ 2 + 2 * a ^ 2) * (-2 * b ^ 2 + 3 * a ^ 2))
    * X ^ 2 - C (b ^ 10 * a ^ 10))

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

def CuboidTwo : Prop := ∀ ⦃a b : ℕ⦄, a.Coprime b → 0 < a → 0 < b → a ≠ b → CuboidTwoFor a b

The second Cuboid conjecture

@[category research open, AMS 12]
theorem declaration uses 'sorry'cuboidTwo : CuboidTwo := by⊢ CuboidTwo
  sorryAll goals completed! 🐙

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

def CuboidThreeFor (a b c : ℤ) : Prop :=
  Irreducible (X ^ 12 + C (6 * c ^ 2 - 2 * a ^ 2 - 2 * b ^ 2) * X ^ 10
    + C (c ^ 4 + b ^ 4 + a ^ 4 + 4 * a ^ 2 * c ^ 2 + 4 * b ^ 2 * c ^ 2 - 12 * b ^ 2 * a ^ 2)
    * X ^ 8 + C (6 * a ^ 4 * c ^ 2 + 6 * c ^ 2 * b ^ 4 - 8 * a ^ 2 * b ^ 2 * c ^ 2
    - 2 * c ^ 4 * a ^ 2 - 2 * c ^ 4 * b ^ 2 - 2 * a ^ 4 * b ^ 2 - 2 * b ^ 4 * a ^ 2)
    * X ^ 6 + C (4 * c ^ 2 * b ^ 4 * a ^ 2 + 4 * a ^ 4 * c ^ 2 * b ^ 2
    - 12 * c ^ 4 * a ^ 2 * b ^ 2 + c ^ 4 * a ^ 4 + c ^ 4 * b ^ 4 + a ^ 4 * b ^ 4) * X ^ 4
    + C (6 * a ^ 4 * c ^ 2 * b ^ 4 - 2 * c ^ 4 * a ^ 4 * b ^ 2 - 2 * c ^ 4 * a ^ 2 * b ^ 4)
    * X ^ 2 + C (c ^ 4 * a ^ 4 * b ^ 4))

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.

def CuboidThree : Prop := ∀ ⦃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 → CuboidThreeFor a b c

The third Cuboid conjecture

@[category research open, AMS 12]
theorem declaration uses 'sorry'cuboidThree : CuboidThree := by⊢ CuboidThree
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 12]
theorem declaration uses 'sorry'cuboid_perfect_euler_brick (h₁ : CuboidOne) (h₂ : CuboidTwo) (h₃ : CuboidThree) :
    ¬ ∃ a b c : ℕ+, IsPerfectCuboid a b c := byh₁:CuboidOneh₂:CuboidTwoh₃:CuboidThree⊢ ¬∃ a b c, IsPerfectCuboid a b c
  sorryAll goals completed! 🐙


end Cuboid


end EulerBrick