Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Dirichlet class number formula, d>0d>0d>0: h(d)=dln⁡εL(1,χ)h(d)=\frac{\sqrt d}{\ln\varepsilon}L(1,\chi)h(d)=lnεd​​L(1,χ)

Open
ClassNumberFormula.dirichlet_class_number_formula_pos

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

class-number-formulanumber-theory

Let d>0d > 0d>0 be a fundamental discriminant, let h(d)h(d)h(d) be the number of proper (SL2(Z)\mathrm{SL}_2(\mathbb Z)SL2​(Z)-) equivalence classes of binary quadratic forms of discriminant ddd, let ε=12(t+ud)\varepsilon = \frac12(t + u\sqrt d)ε=21​(t+ud​) where t>0t>0t>0, u>0u>0u>0 is the solution of t2−du2=4t^2 - du^2 = 4t2−du2=4 with uuu minimal, and let χ\chiχ be the Dirichlet character modulo ddd given by χ(n)=(dn)\chi(n) = \left(\frac{d}{n}\right)χ(n)=(nd​). Then

h(d)=dln⁡ε L(1,χ).h(d) = \frac{\sqrt d}{\ln \varepsilon}\,L(1,\chi).h(d)=lnεd​​L(1,χ).

This is Dirichlet's class number formula for real quadratic discriminants.

Formalization Note The source PDF prints d2ln⁡εL(1,χ)\frac{\sqrt d}{2\ln\varepsilon}L(1,\chi)2lnεd​​L(1,χ). With h(d)h(d)h(d) and ε\varepsilonε defined as in the source, that constant is off by a factor 222: for d=5d=5d=5 one has h(5)=1h(5)=1h(5)=1, ε=3+52\varepsilon=\frac{3+\sqrt5}{2}ε=23+5​​ and L(1,χ)=25ln⁡1+52L(1,\chi)=\frac{2}{\sqrt5}\ln\frac{1+\sqrt5}{2}L(1,χ)=5​2​ln21+5​​, so 5ln⁡εL(1,χ)=1\frac{\sqrt5}{\ln\varepsilon}L(1,\chi)=1lnε5​​L(1,χ)=1, while the printed formula gives 12\frac1221​. The statement here follows Davenport, Multiplicative Number Theory, Ch. 6, the exposition the source says it follows: h(d)ln⁡ε=d L(1,χ)h(d)\ln\varepsilon = \sqrt d\,L(1,\chi)h(d)lnε=d​L(1,χ).

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

theorem dirichlet_class_number_formula_pos (d : ℤ) (hd : IsFundamentalDiscriminant d)
    (hpos : 0 < d) [NeZero d.natAbs] (χ : DirichletCharacter ℂ d.natAbs)
    (hχ : ∀ n : ℕ, χ n = (kroneckerSymbol d n : ℂ)) :
    (formClassNumber d : ℂ) =
      ((Real.sqrt d / Real.log (pellEpsilon d) : ℝ) : ℂ) * χ.LFunction 1 := 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 "Dirichlet class number formula", displayed formula for h(d)h(d)h(d), case d>0d>0d>0 — corrected constant, following H. Davenport, Multiplicative Number Theory, 3rd ed., GTM 74, Springer 2000, Ch. 6 (pp. 43–53)
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me