lean_workbook_plus_24593
ProvedIf $ \frac{x-1}{2} = \frac{y+1}{2} = \frac{z-2}{3}=t $, then we have $ x=2t+1,y=2t-1,z=3t+2 $, so $ xy+yz+zx=f(t)=16t^2+8t-1 $, and this quadratic equation have minimum for $ t=-\frac{1}{4} $.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24593 (x y z t : ℝ) (h₀ : x = 2 * t + 1) (h₁ : y = 2 * t - 1) (h₂ : z = 3 * t + 2) (h₃ : 0 < t) : x * y + y * z + z * x ≥ 16 * t^2 + 8 * t - 1 := by sorry
Source