Prove2Me

Lean-Workbook Syntax 75557: Six equals the sum of its proper divisors

Proved
WorkbookSyntax.plus_75557

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

lean-workbookrepaired-notationsource-checked

The positive proper divisors of 66 sum to 66.

Source: Lean-Workbook row lean_workbook_plus_75557 (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_75557 :
  ∑ k ∈ (Nat.properDivisors 6), k = 6   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_75557; immutable original Prove2Me node cf63f91e-d215-4fb6-8854-b8ef0c919f11

View graph