Prove2Me

Lean-Workbook Plus 27624: Logarithmic identity

Proved
WorkbookRestored.plus_27624

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

lean-workbookrestored-importssource-checked

(log⁡23)(log⁡34)(log⁡45)(log⁡56)=log⁡26(\log_2 3)(\log_3 4)(\log_4 5)(\log_5 6)=\log_2 6.

Source: Lean-Workbook row lean_workbook_plus_27624 (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_27624 : (Real.logb 2 3) * (Real.logb 3 4) * (Real.logb 4 5) * (Real.logb 5 6) = Real.logb 2 6   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_27624; immutable original Prove2Me node 533ec740-f80c-4d30-938c-7f9fd8382698

View graph