sigma_three_twelve
plain-language theorem explainer
σ_3(12) evaluates to 2044. Researchers verifying explicit divisor power sums in arithmetic function libraries would cite this for numerical checks. The proof is a one-line term reduction via native_decide that evaluates the sum directly.
Claim. Let $σ_k(n)$ denote the sum of the $k$th powers of the positive divisors of the positive integer $n$. Then $σ_3(12) = 2044$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Statements remain minimal until deeper Dirichlet algebra is added. The sigma function, defined in the same module, computes sums of divisor powers; the theorem applies it to the specific case k=3 and n=12.
proof idea
The proof is a one-line term wrapper that applies native_decide to reduce the equality sigma 3 12 = 2044 to a decidable computation.
why it matters
This supplies a verified numerical value for σ_3(12) inside the arithmetic functions module of NumberTheory.Primes. It anchors explicit calculations without listed downstream uses. The result fits the framework's pattern of concrete evaluations that support later prime and divisor work, consistent with lightweight interfaces noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.