Prove2Me

lean_workbook_plus_51489

Open

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

Prove f(a):=1−1a−ln⁡a<0f(a):=1-\frac 1a-\ln a<0 for a>1a>1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_51489 (a : ℝ) (ha : 1 < a) : 1 - (1 / a) - Real.log a < 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph