TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The summatory divisor-sum function is pi squared over 12 times x squared plus O(x log x)

Statement

For every real $x \geq 1$ ,

$\sum_{n \leq x} σ (n) = \frac{π^{2}}{12} x^{2} + O (x \log x) .$

Facts & Assumptions

Given: A real $x \geq 1$ , an integer $M : = ⌊ x ⌋$ , and $y_{m} : = ⌊ x / m ⌋$ for $1 \leq m \leq M$ .

Proof

technique · direct

1.1givenalgebra

By The divisor functions arise by Dirichlet convolution, $σ (n) = \sum_{d ∣ n} d$ . Summing over $n \leq x$ and writing each such $n$ as $d m$ gives $\sum_{n \leq x} σ (n) = \sum_{m = 1}^{M} \sum_{d = 1}^{y_{m}} d .$

2.1step 1.1givenalgebra

For each $m$ , $\sum_{d = 1}^{y_{m}} d = \frac{y_{m} (y_{m} + 1)}{2} = \frac{y_{m}^{2}}{2} + O (y_{m}) .$ Therefore $\sum_{n \leq x} σ (n) = \frac{1}{2} \sum_{m = 1}^{M} y_{m}^{2} + O ⁣ (\sum_{m = 1}^{M} y_{m}) .$

3.1step 2.1givenalgebra

Since $y_{m} = x / m + O (1)$ uniformly in $m$ , one has $y_{m}^{2} = x^{2} / m^{2} + O (x / m) + O (1)$ . Summing and using The Basel sum is pi squared over six by a residue computation together with The harmonic sum is log x plus gamma plus O(1/x) gives $\sum_{m = 1}^{M} y_{m}^{2} = \frac{π^{2}}{6} x^{2} + O (x \log x), \sum_{m = 1}^{M} y_{m} = O (x \log x) .$

4.1step 2.1step 3.1givenalgebra∎

Substituting step 3.1 into step 2.1 yields $\sum_{n \leq x} σ (n) = \frac{π^{2}}{12} x^{2} + O (x \log x) .$

Depends on

Used by

The average order of sigma is (pi squared over 6)n Corollary

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Karl-Dieter Crisman, Number Theory: In Context and Interactive (standard reference, not scraped)