lean_workbook_plus_68369

Proved

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

Let $a=10^{1965}$ , $A=\frac{a+1}{10a+1}$ , and $B=\frac{10a+1}{100a+1}$ . Prove that $A > B$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68369 (a A B : ℝ) (ha : a = 10^1965) (hA : A = (a + 1) / (10 * a + 1)) (hB : B = (10 * a + 1) / (100 * a + 1)) : A > B   :=  by sorry

Source

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

View graph