Prove2Me

lean_workbook_plus_731

Disproved

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

a+ba2+b+b+cb+c2≤2((a+b)2a2+b+(b+c)2b+c2)≤2.\frac{a+b}{\sqrt{a^{2}+b}} + \frac{b+c}{\sqrt{b+c^{2}}} \leq \sqrt{2\left(\frac{(a+b)^2}{a^{2}+b} + \frac{(b+c)^2}{b+c^{2}} \right)}\leq2.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_731 : ∀ a b c : ℝ, (a + b) / Real.sqrt (a ^ 2 + b) + (b + c) / Real.sqrt (b + c ^ 2) ≤ Real.sqrt (2 * ((a + b) ^ 2 / (a ^ 2 + b) + (b + c) ^ 2 / (b + c ^ 2))) ∧ Real.sqrt (2 * ((a + b) ^ 2 / (a ^ 2 + b) + (b + c) ^ 2 / (b + c ^ 2))) ≤ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph