Lean-Workbook Plus 50350: Logarithmic inequality

Proved

WorkbookRestored.plus_50350

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

lean-workbookrestored-importssource-checked

For real $x>1$ , $\log\bigl(x(x^2+3)/(3x^2+1)\bigr)<x$ .

Source: Lean-Workbook row lean_workbook_plus_50350 (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_50350 (x : ℝ) (hx : 1 < x) : Real.log (x * (x ^ 2 + 3) / (3 * x ^ 2 + 1)) < x   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_50350; immutable original Prove2Me node 5fcc9b70-0f5b-4f1c-8f80-f9f495bda15d

View graph