Lean-Workbook Plus 25042: Logarithmic identity

Proved

WorkbookRestored.plus_25042

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

lean-workbookrestored-importssource-checked

$\log_2(\log_4 16)=1$ .

Source: Lean-Workbook row lean_workbook_plus_25042 (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.Base
open Real

Formal statement

theorem WorkbookRestored.plus_25042 :
  Real.logb 2 (Real.logb 4 16) = 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_25042; immutable original Prove2Me node f9fa5271-f644-4bb8-93e8-76f0d7078e4b

View graph