Prove2Me

Lean-Workbook Plus 54169: Logarithmic inequality

Proved
WorkbookRestored.plus_54169

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

(1+ln⁡x)ln⁡x+1x>0(1+\ln x)\ln x+\frac1x>0 for all x>0x>0.

Source: Lean-Workbook row lean_workbook_plus_54169 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_54169 (x : ℝ) (hx : 0 < x) : (1 + Real.log x) * Real.log x + 1 / x > 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_54169; immutable original Prove2Me node 3f940383-19dd-4bda-8896-b1543cfa2bd0

View graph