Prove2Me

Zeta function of y2+y=x5y^2+y=x^5 over F41\mathbb F_{41}

Proved
WeilConjectures.hyperelliptic_F41_zeta

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

hyperelliptic-curvesnumber-theoryzeta-function

For C:y2+y=x5C: y^2+y=x^5 over F41\mathbb F_{41} (genus 2, one point at infinity), let Nm=#{(x,y)∈F41m2:y2+y=x5}+1N_m=\#\{(x,y)\in\mathbb F_{41^m}^2: y^2+y=x^5\}+1. Then

ζ(C/F41,s)=P1(T)P0(T)P2(T)=1−9T+71T2−9⋅41 T3+412T4(1−T)(1−41T),T=41−s.\zeta(C/\mathbb F_{41},s)=\frac{P_1(T)}{P_0(T)P_2(T)}=\frac{1-9T+71T^2-9\cdot41\,T^3+41^2T^4}{(1-T)(1-41T)},\qquad T=41^{-s}.

This is the source's worked example of rationality for a curve of genus 2.

Formalization Note The zeta function is zetaOfCounts applied to the counts NmN_m above, with F41m\mathbb F_{41^m} = FiniteField.Extension (ZMod 41) 41 m; the identity is stated as Z⋅(1−T)(1−41T)=P1(T)Z\cdot(1-T)(1-41T)=P_1(T) in Q[[T]]\mathbb Q[[T]]. The point count of the smooth projective model is encoded as affine solutions plus one point at infinity, as in the source.

Preamble
import Mathlib
import Definitions.Def_WeilConjectures_projectiveSpace
import Definitions.Def_WeilConjectures_zetaFunction

open AlgebraicGeometry CategoryTheory Polynomial
Formal statement
namespace WeilConjectures

theorem hyperelliptic_F41_zeta [Fact (Nat.Prime 41)] :
    zetaOfCounts (fun m => if h : m = 0 then 0 else
        haveI : NeZero m := ⟨h⟩
        Nat.card {xy : FiniteField.Extension (ZMod 41) 41 m × FiniteField.Extension (ZMod 41) 41 m //
          xy.2 ^ 2 + xy.2 = xy.1 ^ 5} + 1) *
      ((1 - PowerSeries.X) * (1 - 41 * PowerSeries.X)) =
    1 - 9 * PowerSeries.X + 71 * PowerSeries.X ^ 2 - 9 * 41 * PowerSeries.X ^ 3 +
      41 ^ 2 * PowerSeries.X ^ 4 := 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", displayed formula for ζ(C/F41,s)\zeta(C/\mathbb F_{41},s)
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