Prove2Me

Lean-Workbook Syntax 36920: Counting the positive divisors of 72

Proved
WorkbookSyntax.plus_36920

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

lean-workbookrepaired-notationsource-checked

The integer 7272 has exactly 1212 positive divisors.

Source: Lean-Workbook row lean_workbook_plus_36920 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.NumberTheory.Divisors
Formal statement
theorem WorkbookSyntax.plus_36920 :
  (∑ k ∈ (Nat.divisors 72), 1) = 12   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_36920; immutable original Prove2Me node 67dacb5b-c9f7-489e-9289-8ef168eb7b2f

View graph