Prove2Me

lean_workbook_plus_20129

Disproved

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

Let a1,a2,⋯ ,an∈(0,1)a_1,a_2 ,\cdots ,a_n \in (0,1) , prove that a1a2⋯an+(1−a1)(1−a2)⋯(1−an)<1.\sqrt{a_1a_2\cdots a_n}+\sqrt{(1-a_1)(1-a_2)\cdots (1-a_n)}<1. (n≥2)(n\ge 2)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20129 : ∀ n : ℕ, 2 ≤ n → ∀ a : Fin n → ℝ, (∀ i, 0 < a i ∧ a i < 1) → Real.sqrt (∏ i, a i) + Real.sqrt (∏ i, (1 - a i)) < 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph