Prove2Me

lean_workbook_plus_21986

Disproved

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

Prove that: a2b2⋅(t1−2t)2+b2c2⋅(r1−2r)2+c2a2⋅(μ1−2μ)2+16trμ≥1\frac {a^2}{b^2} \cdot \left( \frac {t}{1 - 2t} \right)^2 + \frac {b^2}{c^2} \cdot \left( \frac {r}{1 - 2r} \right)^2 + \frac {c^2}{a^2} \cdot \left( \frac {\mu}{1 - 2\mu} \right)^2 + 16tr \mu \geq 1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21986 :  ∀ a b c t r μ : ℝ, (a^2 / b^2 * (t / (1 - 2 * t))^2 + b^2 / c^2 * (r / (1 - 2 * r))^2 + c^2 / a^2 * (μ / (1 - 2 * μ))^2 + 16 * t * r * μ) ≥ 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph