Can `nlinarith` prove the Motzkin polynomial positive?

Stream: mathlib4

[Bolton Bailey]

I was telling a cryptographer at a conference about Lean and showing him some goals that can be proved by linarith. he asked if it could prove the "Motzkin polynomial" positive 0 < 1 - 3 * x^2 * y^2 + x^2 * y^4 + x^4 * y^2, which I guess has the distinction of not being a sum of squares of polynomials. I figured I would ask here if there is something special I can do to get nlinarith to prove this positive.

[Kim Morrison]

Seems pretty unlikely!

[Jeremy Tan]

Well, this is the textbook way of proving it:

import Mathlib.Analysis.MeanInequalities

open Real

theorem motzkin_polynomial_nonneg {x y : ℝ} :
    0 ≤ 1 - 3 * x ^ 2 * y ^ 2 + x ^ 2 * y ^ 4 + x ^ 4 * y ^ 2 := by
  have nn₁ : 0 ≤ x ^ 2 * y ^ 4 := by positivity
  have nn₂ : 0 ≤ x ^ 4 * y ^ 2 := by positivity
  have key := geom_mean_le_arith_mean3_weighted (by norm_num) (by norm_num) (by norm_num)
    nn₁ nn₂ zero_le_one (add_thirds 1)
  rw [one_rpow, mul_one, ← Real.mul_rpow nn₁ nn₂, ← mul_add, ← mul_add,
    show x ^ 2 * y ^ 4 * (x ^ 4 * y ^ 2) = (x ^ 2) ^ 3 * (y ^ 2) ^ 3 by ring,
    Real.mul_rpow (by positivity) (by positivity),
    ← Real.rpow_natCast _ 3, ← Real.rpow_mul (sq_nonneg x),
    ← Real.rpow_natCast _ 3, ← Real.rpow_mul (sq_nonneg y),
    show ((3 : ℕ) * ((1 : ℝ) / 3)) = 1 by norm_num, rpow_one, rpow_one] at key
  linarith

[Kim Morrison]

@Jeremy Tan, you should PR this somewhere! If someone also wanted to prove that it is not a sum of squares then it would be a great candidate for Counterexamples/.

[Jeremy Tan]

#23170