Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Finite form of L(1,χ)L(1,\chi)L(1,χ) for prime conductor q≡1(mod4)q\equiv1\pmod 4q≡1(mod4)

Proved
ClassNumberFormula.L_one_finite_form_one_mod_four

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

class-number-formulanumber-theory

Let qqq be a prime with q≡1(mod4)q\equiv 1\pmod 4q≡1(mod4), and let χ\chiχ be the Dirichlet character modulo qqq given by the Legendre symbol, χ(m)=(mq)\chi(m) = \left(\frac{m}{q}\right)χ(m)=(qm​). Then

L(1,χ)=−1q1/2∑m=1q−1(mq)ln⁡(sin⁡mπq).L(1,\chi) = -\frac{1}{q^{1/2}}\sum_{m=1}^{q-1}\left(\frac{m}{q}\right)\ln\left(\sin\frac{m\pi}{q}\right).L(1,χ)=−q1/21​m=1∑q−1​(qm​)ln(sinqmπ​).

Combined with the case d=qd = qd=q of Dirichlet's formula, this gives a finite expression for the class number in terms of logarithms of sines.

Formalization Note The source PDF prints the constant −12q1/2-\frac{1}{2q^{1/2}}−2q1/21​. With the sum over all m=1,…,q−1m=1,\dots,q-1m=1,…,q−1 that constant is off by a factor 222: for q=5q=5q=5, L(1,χ)=25ln⁡1+52≈0.4304L(1,\chi)=\frac{2}{\sqrt5}\ln\frac{1+\sqrt5}{2}\approx0.4304L(1,χ)=5​2​ln21+5​​≈0.4304, while −15∑m=14(m5)ln⁡sin⁡mπ5≈0.4304-\frac{1}{\sqrt5}\sum_{m=1}^{4}\left(\frac m5\right)\ln\sin\frac{m\pi}{5}\approx0.4304−5​1​∑m=14​(5m​)lnsin5mπ​≈0.4304 and the printed constant gives half of this. The statement here uses −1q1/2-\frac{1}{q^{1/2}}−q1/21​. In the source, χ=(d⋅)\chi = \left(\frac{d}{\cdot}\right)χ=(⋅d​) with d=qd = qd=q, which equals (mq)\left(\frac{m}{q}\right)(qm​) by quadratic reciprocity.

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

theorem L_one_finite_form_one_mod_four (q : ℕ) [Fact q.Prime] (hq : q % 4 = 1)
    (χ : DirichletCharacter ℂ q) (hχ : ∀ m : ℕ, χ m = (legendreSym q m : ℂ)) :
    χ.LFunction 1 = ((-(1 / Real.sqrt q) * ∑ m ∈ Finset.Ico 1 q,
      (legendreSym q m : ℝ) * Real.log (Real.sin (m * π / q)) : ℝ) : ℂ) := 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", last displayed formula, case q≡1(mod4)q \equiv 1 \pmod 4q≡1(mod4) — corrected constant, see Formalization Note
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