--- /dev/null
+++ b/Mathlib/Unsorry/QuarticFourVarGeFourProd.lean
@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2026 Chris Barlow. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Barlow
+-/
+import Mathlib
+
+theorem quartic_four_var_ge_four_prod (a b c d : ℝ) :
+    4 * a * b * c * d ≤ a ^ 4 + b ^ 4 + c ^ 4 + d ^ 4 := by
+  nlinarith [sq_nonneg (a ^ 2 - b ^ 2), sq_nonneg (c ^ 2 - d ^ 2), sq_nonneg (a * b - c * d),
+    sq_nonneg (a * b + c * d)]