Prove2Me

An inequality from a product of adjacent sums

Proved
WorkbookCorrected.plus_27672

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Let 0<a,b,c<10<a,b,c<1 satisfy (a+b)(b+c)=1(a+b)(b+c)=1. Then

b2≥(1−a)(1−c).b^2\ge(1-a)(1-c).

Formalization Note: The source formalization added a+b+c=1a+b+c=1, an assumption absent from the source and incompatible with its other hypotheses. This correction removes that added assumption and proves the stated inequality from the original interval and product conditions.

Source: InternLM Lean-Workbook, record lean_workbook_plus_27672 (Apache-2.0).

Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_27672 (a b c : ℝ) (ha : 0<a ∧ a<1) (hb : 0<b ∧ b<1) (hc : 0<c ∧ c<1) (h : (a+b)*(b+c)=1) : b^2 ≥ (1-a)*(1-c) := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_27672; Apache-2.0

View graph