Prove2Me

Lattice points in a quarter circle: count ∼π4N\sim \frac{\pi}{4} N

Proved
ClassNumberFormula.quarter_circle_lattice_count

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

class-number-formulanumber-theory

The number of lattice points in the quarter disc of radius N\sqrt N satisfies

lim⁡N→∞#{(a,b)∈Z2:a>0, b≥0, a2+b2≤N}N=π4.\lim_{N\to\infty}\frac{\#\{(a,b)\in\mathbb Z^2 : a > 0,\ b\ge0,\ a^2+b^2\le N\}}{N} = \frac{\pi}{4}.

This is the lattice-point estimate from the Gauss circle problem, and it gives the average of the coefficients of ζQ(i)\zeta_{\mathbb Q(i)}.

Formalization Note The quarter disc is taken with a>0a>0, b≥0b\ge0, which matches the coefficient count in the preceding milestone; any choice of boundary gives the same limit.

Preamble
import Mathlib
open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real
Formal statement
namespace ClassNumberFormula

theorem quarter_circle_lattice_count :
    Tendsto (fun N : ℕ =>
        (Nat.card {p : ℤ × ℤ // 0 < p.1 ∧ 0 ≤ p.2 ∧ p.1 ^ 2 + p.2 ^ 2 ≤ N} : ℝ) / N)
      atTop (𝓝 (π / 4)) := 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 ("approximating the number of lattice points inside of a quarter circle centered at the origin"); see also the Gauss circle problem
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