$K=\mathbb Q(i)$ : the coefficients of $\zeta_K$ count sums of two squares

Proved

ClassNumberFormula.gaussian_ideal_count_eq_two_squares

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

class-number-formulanumber-theory

Let $K$ be a quadratic number field containing a square root of $-1$ , that is, $K \cong \mathbb Q(i)$ , whose ring of integers is the Gaussian integers. Then for every $n\ge1$ the $n$ -th coefficient of $\zeta_K$ , the number of ideals of norm $n$ , is

\#\{\mathfrak a \subseteq \mathcal O_K : N(\mathfrak a) = n\} = \#\{(a,b)\in\mathbb Z^2 : a > 0,\ b \ge 0,\ a^2 + b^2 = n\}.

The right-hand side is one quarter of the number $r_2(n)$ of representations of $n$ as a sum of two squares of integers. This makes precise the source's remark that the coefficient is "essentially the number of representations of $n$ as a sum of two squares of nonnegative integers".

Formalization Note The source's "essentially" is made exact by counting pairs with $a > 0$ , $b \ge 0$ (one representative per unit class $\{\pm1,\pm i\}$ ); counting pairs of non-negative integers instead would overcount, e.g. for $n = 1$ .

Preamble

import Mathlib
open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real

Formal statement

namespace ClassNumberFormula

theorem gaussian_ideal_count_eq_two_squares (K : Type*) [Field K] [NumberField K]
    (hK : Module.finrank ℚ K = 2) (hi : ∃ i : K, i ^ 2 = -1) (n : ℕ) (hn : 1 ≤ n) :
    Nat.card {I : Ideal (𝓞 K) // Ideal.absNorm I = n} =
      Nat.card {p : ℤ × ℤ // 0 < p.1 ∧ 0 ≤ p.2 ∧ p.1 ^ 2 + p.2 ^ 2 = n} := by sorry

end ClassNumberFormula

Source

Wikipedia, "Class number formula" (revision oldid=1366411311), https://en.wikipedia.org/w/index.php?title=Class_number_formula&oldid=1366411311, section "Proof", second paragraph ("The n-th coefficient of the Dirichlet series is essentially the number of representations of n as a sum of two squares")

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

K=Q(i)K=\mathbb Q(i)K=Q(i): the coefficients of ζK\zeta_KζK​ count sums of two squares

$K=\mathbb Q(i)$ : the coefficients of $\zeta_K$ count sums of two squares