lean_workbook_plus_79483

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Min: Suppose that: $x\ge y\ge z \Rightarrow 3x^4\ge x^4+y^4+z^4=1 \Rightarrow x^2\ge \frac{\sqrt{3}}{3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79483 :  ∀ x y z : ℝ, x ≥ y ∧ y ≥ z ∧ 3 * x ^ 4 ≥ x ^ 4 + y ^ 4 + z ^ 4 ∧ x ^ 4 + y ^ 4 + z ^ 4 = 1 → x ^ 2 ≥ Real.sqrt 3 / 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph