lean_workbook_plus_65235Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)3x4+1≥4x33x^4+1\geq 4x^33x4+1≥4x3 is true for all reals though. 3x4−4x3+1≥03x^4-4x^3+1 \geq 03x4−4x3+1≥0 (x−1)2(3x2+2x+1)≥0(x-1)^2(3x^2+2x+1) \geq 0(x−1)2(3x2+2x+1)≥0 (x−1)2(3(x+13)2+23)≥0(x-1)^2(3(x+\frac{1}{3})^2+\frac{2}{3})\geq 0(x−1)2(3(x+31)2+32)≥0 . This is clearly true and only reaches equality when x=1x=1x=1 .Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_65235 (x : ℝ) : 3 * x^4 + 1 ≥ 4 * x^3 := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph