Prove2Me

Lean-Workbook Syntax 51761: Counting the positive divisors of 576

Proved
WorkbookSyntax.plus_51761

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

lean-workbookrepaired-notationsource-checked

The integer 576576 has exactly 2121 positive divisors.

Source: Lean-Workbook row lean_workbook_plus_51761 (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.NumberTheory.Divisors
Formal statement
theorem WorkbookSyntax.plus_51761 :
  (∑ k ∈ (Nat.divisors 576), 1) = 21   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_51761; immutable original Prove2Me node fd667cd0-6a7e-4473-b4e6-4b1c3624b38d

View graph