Skip to content

feat: cuboid conjectures #1850

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
felixpernegger wants to merge 10 commits into
base: main
Choose a base branch
from
Open

feat: cuboid conjectures #1850

Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
3302e3c
cuboid to euler
felixpernegger Jan 22, 2026
e674b95
cuboid to euler brick
felixpernegger Jan 22, 2026
9446a0d
Update FormalConjectures/Wikipedia/EulerBrick.lean
felixpernegger Jan 22, 2026
3798c8d
add docstrings
felixpernegger Jan 22, 2026
50d3057
wrong exponent
felixpernegger Jan 22, 2026
dc0e5b4
Merge branch 'main' into cuboid
felixpernegger Jan 22, 2026
a2f8219
fix
felixpernegger Jan 22, 2026
e5fd032
Update FormalConjectures/Wikipedia/EulerBrick.lean
felixpernegger Jan 23, 2026
9137443
apply suggestions
felixpernegger Jan 23, 2026
fbc12b5
fix copyright?
felixpernegger Jan 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
88 changes: 79 additions & 9 deletions FormalConjectures/Wikipedia/EulerBrick.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ 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 FormalConjectures.Util.ProblemImports

/-!
Expand All @@ -22,6 +21,7 @@ import FormalConjectures.Util.ProblemImports
*References:*
- [Wikipedia](https://en.wikipedia.org/wiki/Euler_brick)
- [stackexchange](https://math.stackexchange.com/questions/2264401/euler-bricks-and-the-4th-dimension)
- [Sh12] Shapirov, Ruslan. Perfect cuboids and irreducible polynomials. https://arxiv.org/abs/1108.5348
-/

namespace EulerBrick
Expand All @@ -30,42 +30,112 @@ 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)
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)
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)
Pairwise fun i j ↦ IsSquare ((sides i)^2 + (sides j)^2)

/--
Is there a perfect Euler brick?
-/
@[category research open, AMS 11]
theorem perfect_euler_brick_existence :
answer(sorry) ↔ ∃ a b c : ℕ+, IsPerfectCuboid a b c := by
sorry
answer(sorry) ↔ ∃ a b c : ℕ+, IsPerfectCuboid a b c := by
sorry

/--
Is there an Euler brick in $4$-dimensional space?
-/
@[category research open, AMS 11]
theorem four_dim_euler_brick_existence :
answer(sorry) ↔ ∃ sides : Fin 4 → ℕ+, IsEulerHyperBrick 4 sides:= by
sorry
answer(sorry) ↔ ∃ sides : Fin 4 → ℕ+, IsEulerHyperBrick 4 sides:= by
sorry

/--
Is there an Euler brick in $n$-dimensional space for any $n > 3$?
-/
@[category research open, AMS 11]
theorem n_dim_euler_brick_existence :
answer(sorry) ↔ ∀ n > 3, ∃ sides : Fin n → ℕ+, IsEulerHyperBrick n sides := by
answer(sorry) ↔ ∀ n > 3, ∃ sides : Fin n → ℕ+, IsEulerHyperBrick n sides := by
sorry

section Cuboid

open Polynomial

/-! **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.
-/

/-- 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 -/
@[category research open, AMS 12]
theorem cuboidOne : CuboidOne := by sorry

/-- 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 cuboidTwo : CuboidTwo := by sorry

/-- 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 cuboidThree : CuboidThree := by sorry

/-- In [Sh12], Ruslan notes that a perfect Euler brick does not exist
if all three Cuboid conjectures hold. -/
@[category research solved, AMS 12]
theorem cuboid_perfect_euler_brick (h₁ : CuboidOne) (h₂ : CuboidTwo) (h₃ : CuboidThree) :
¬ ∃ a b c : ℕ+, IsPerfectCuboid a b c := by
sorry

end Cuboid

end EulerBrick
Loading