lean_workbook_plus_3696

Disproved

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

Show that for $a,b,c$ in real numbers, such that $a^{2}+b^{2}+c^{2}=3$ , then $\frac{1}{1+2ab}+\frac{1}{1+2bc}+\frac{1}{1+2ca}\geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3696 : ∀ a b c : ℝ, a^2 + b^2 + c^2 = 3 → 1 / (1 + 2 * a * b) + 1 / (1 + 2 * b * c) + 1 / (1 + 2 * c * a) ≥ 1   :=  by sorry

Source

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

View graph