Prove2Me

lean_workbook_plus_7090

Disproved

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

For positives aa , bb and cc we obtain\n\n∑cyca∑cyc11+a2≥∑cyca21+a2∑cyc1a⇔∑cyca∑cyc11+a2≥(3−∑cyc11+a2)∑cyc1a⇔\sum_{cyc}a\sum_{cyc}\frac{1}{1+a^2}\geq\sum_{cyc}\frac{a^2}{1+a^2}\sum_{cyc}\frac{1}{a}\Leftrightarrow\sum_{cyc}a\sum_{cyc}\frac{1}{1+a^2}\geq\left(3-\sum_{cyc}\frac{1}{1+a^2}\right)\sum_{cyc}\frac{1}{a}\Leftrightarrow\n\n⇔∑cyc(a+1a)∑cyc11+a2≥3∑cyc1a⇔∑cyc(1+a2a(1+b2)+1+a2a(1+c2))≥2∑cyc1a⇔\Leftrightarrow\sum_{cyc}\left(a+\frac{1}{a}\right)\sum_{cyc}\frac{1}{1+a^2}\geq3\sum_{cyc}\frac{1}{a}\Leftrightarrow\sum_{cyc}\left(\frac{1+a^2}{a(1+b^2)}+\frac{1+a^2}{a(1+c^2)}\right)\geq2\sum_{cyc}\frac{1}{a}\Leftrightarrow\n\n⇔∑cyc(1+a2a(1+b2)+1+b2b(1+a2)−1a−1b)≥⇔∑cyc(a2−b2)(1a(1+b2)−1b(1+a2))≥0⇔\Leftrightarrow\sum_{cyc}\left(\frac{1+a^2}{a(1+b^2)}+\frac{1+b^2}{b(1+a^2)}-\frac{1}{a}-\frac{1}{b}\right)\geq\Leftrightarrow\sum_{cyc}(a^2-b^2)\left(\frac{1}{a(1+b^2)}-\frac{1}{b(1+a^2)}\right)\geq0\Leftrightarrow\n\n⇔∑cyc(a−b)2(a+b)(ab−1)ab(1+a2)(1+b2)≥0\Leftrightarrow\sum_{cyc}\frac{(a-b)^2(a+b)(ab-1)}{ab(1+a^2)(1+b^2)}\geq0 . Done!

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7090 :
  ∀ a b c : ℝ, 0 < a ∧ 0 < b ∧ 0 < c →
  (a + b + c) * (1 / (1 + a^2) + 1 / (1 + b^2) + 1 / (1 + c^2)) ≥
    (a^2 / (1 + a^2) + b^2 / (1 + b^2) + c^2 / (1 + c^2)) * (1 / a + 1 / b + 1 / c)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph