lean_workbook_plus_34062

Disproved

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

Let $a=kx$ , $b=ky$ , where $x^2+xy+y^2=1$ and $k\geq 1$ . Prove that $a^2+b^2+ab<1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34062 (a b k x y : ℝ) (h₁ : a = k * x) (h₂ : b = k * y) (h₃ : x^2 + x * y + y^2 = 1) (h₄ : k ≥ 1) : a^2 + b^2 + a * b < 1   :=  by sorry

Source

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

View graph