Lean-Workbook Plus 68777: Totient of 462

Proved

WorkbookRestored.plus_68777

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

lean-workbookrestored-importssource-checked

$\varphi(462)=120$ . Thus 120 integers from 1 through 462 are coprime to 462.

Source: Lean-Workbook row lean_workbook_plus_68777 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Data.Nat.Totient

Formal statement

theorem WorkbookRestored.plus_68777 :
  Nat.totient 462 = 120   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_68777; immutable original Prove2Me node a93df8b9-2e87-4bb7-a25f-029eb34d24d8

View graph