lean_workbook_plus_17318

Disproved

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

Prove that $(\dfrac{1}{a}+\dfrac{2\sqrt2}{c})(\dfrac{1}{a}+\dfrac{2\sqrt2}{c})(a^2+c^2)\geq (1+2)^3=27$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17318 : ∀ a c : ℝ, (1 / a + 2 * Real.sqrt 2 / c) * (1 / a + 2 * Real.sqrt 2 / c) * (a ^ 2 + c ^ 2) ≥ 27   :=  by sorry

Source