Prove2Me

lean_workbook_plus_25471

Disproved

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

23−16≤(1−a)(1−b)+a1+2b+b1+2a≤1\sqrt{\frac{2}{3}}-\frac{1}{6} \le (1-a)(1-b)+\frac{a}{1+2b}+\frac{b}{1+2a}\le 1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25471 : ∀ a b : ℝ, Real.sqrt (2 / 3) - 1 / 6 ≤ (1 - a) * (1 - b) + a / (1 + 2 * b) + b / (1 + 2 * a) ∧ (1 - a) * (1 - b) + a / (1 + 2 * b) + b / (1 + 2 * a) ≤ 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph