lean_workbook_plus_75557

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Even if you didn't know that $6$ is a perfect number, you could easily find that the divisors of $6$ excluding itself are $1,2,3$ and the sum is $1+2+3=\boxed{6}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75557 :
  ∑ k in (Nat.properDivisors 6), k = 6   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph