lean_workbook_plus_6524

Proved

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

Let $a$ and $b$ be real numbers such that $3\le a^2+ab+b^2\le6$ . Prove that $2\le a^4+b^4\le72 .$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6524 (a b : ℝ) (h1 : 3 ≤ a ^ 2 + b ^ 2 + a * b) (h2 : a ^ 2 + b ^ 2 + a * b ≤ 6) : 2 ≤ a ^ 4 + b ^ 4 ∧ a ^ 4 + b ^ 4 ≤ 72   :=  by sorry

Source

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

View graph