Riemann hypothesis for $P_1(T)=1-9T+71T^2-369T^3+1681T^4$

Proved

WeilConjectures.hyperelliptic_F41_riemann_hypothesis

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

number-theorypolynomials

The polynomial $P_1(T)=1-9T+71T^2-9\cdot41\,T^3+41^2T^4$ factors over $\mathbb C$ as

P_1(T)=\prod_{j=1}^4(1-\alpha_{1,j}T)\qquad\text{with}\qquad|\alpha_{1,j}|=\sqrt{41}\ \ (j=1,2,3,4).

This is the Riemann hypothesis part of the Weil conjectures for the curve $y^2+y=x^5$ over $\mathbb F_{41}$ .

Formalization Note The $\alpha_{1,j}$ are a multiset of four complex numbers.

Preamble

import Mathlib
import Definitions.Def_WeilConjectures_projectiveSpace
import Definitions.Def_WeilConjectures_zetaFunction

open AlgebraicGeometry CategoryTheory Polynomial

Formal statement

namespace WeilConjectures

theorem hyperelliptic_F41_riemann_hypothesis  :
    ∃ α : Multiset ℂ, Multiset.card α = 4 ∧
      (1 - 9 * Polynomial.X + 71 * Polynomial.X ^ 2 - 9 * 41 * Polynomial.X ^ 3 +
          41 ^ 2 * Polynomial.X ^ 4 : ℂ[X]) = (α.map fun a => 1 - C a * Polynomial.X).prod ∧
      ∀ a ∈ α, ‖a‖ = Real.sqrt 41 := by sorry

end WeilConjectures

Source

Wikipedia, "Weil conjectures", https://en.wikipedia.org/wiki/Weil_conjectures (PDF snapshot supplied by the proposer, 14 pp.), section "Examples", subsection "Hyperelliptic curves" (

|\alpha_{1,j}|=\sqrt{41}

for

j=1,2,3,4

)

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

Riemann hypothesis for P1(T)=1−9T+71T2−369T3+1681T4P_1(T)=1-9T+71T^2-369T^3+1681T^4P1​(T)=1−9T+71T2−369T3+1681T4

Riemann hypothesis for $P_1(T)=1-9T+71T^2-369T^3+1681T^4$