lean_workbook_plus_54224

Proved

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

Show that $A = \frac{2^{2009}+1}{2^{2010}+1} > B = \frac{2^{2010}+1}{2^{2011}+1}$ algebraically

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54224 (A B : ℝ) (h₁ : A = (2^(2009:ℕ) + 1) / (2^(2010:ℕ) + 1)) (h₂ : B = (2^(2010:ℕ) + 1) / (2^(2011:ℕ) + 1)) : A > B   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph