diff --git a/FormalConjectures/Wikipedia/EulerBrick.lean b/FormalConjectures/Wikipedia/EulerBrick.lean
index c74a2867c..ba1a504f2 100644
--- a/FormalConjectures/Wikipedia/EulerBrick.lean
+++ b/FormalConjectures/Wikipedia/EulerBrick.lean
@@ -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
 
 /-!
@@ -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
@@ -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