lean_workbook_plus_50464

Open

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

Let $\log_23 =x, 1<x<2$ (can easy be proved, that $\frac{3}{2}<x<\frac{8}{5})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50464 : 1 < Real.log 3 / Real.log 2 ∧ Real.log 3 / Real.log 2 < 2   :=  by sorry

Source