Prove2Me

Lean-Workbook Plus 77334: Euler’s totient at fifteen

Proved
WorkbookRestored.plus_77334

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

lean-workbookrestored-importssource-checked

φ(15)=8\varphi(15)=8.

Source: Lean-Workbook row lean_workbook_plus_77334 (Apache-2.0), original record. This repair only restores required imports and namespaces; the mathematical declaration is unchanged.

Preamble
import Mathlib.Data.Nat.Totient
open Nat
Formal statement
theorem WorkbookRestored.plus_77334 (n : ℕ) (h : n = 15) : φ n = 8   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_77334; immutable original Prove2Me node ce767a9d-3bfe-496d-8797-95a0d3fc1b7f

View graph