$y^2+y=x^5$ over $\mathbb F_{41}$ : $N_1=33$ , $N_2=1743$

Proved

WeilConjectures.hyperelliptic_F41_point_counts

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

finite-fieldshyperelliptic-curvesnumber-theory

Consider the genus-2 hyperelliptic curve $C: y^2+y=x^5$ over $\mathbb F_{41}$ . Counting affine solutions $(x,y)$ over $\mathbb F_{41}$ and $\mathbb F_{41^2}$ and adding one point at infinity gives

N_1=\#\{(x,y)\in\mathbb F_{41}^2: y^2+y=x^5\}+1=33,\qquad N_2=\#\{(x,y)\in\mathbb F_{41^2}^2: y^2+y=x^5\}+1=1743.

These counts determine the coefficients $c_1=N_1-1-q=-9$ and $c_2=(N_2-1-q^2+c_1^2)/2=71$ of the Weil polynomial $P_1$ .

Formalization Note $\mathbb F_{41}$ is ZMod 41 and $\mathbb F_{41^2}$ is GaloisField 41 2; the primality of 41 is supplied as a Fact instance argument.

Preamble

import Mathlib
import Definitions.Def_WeilConjectures_projectiveSpace
import Definitions.Def_WeilConjectures_zetaFunction

open AlgebraicGeometry CategoryTheory Polynomial

Formal statement

namespace WeilConjectures

theorem hyperelliptic_F41_point_counts [Fact (Nat.Prime 41)] :
    Nat.card {xy : ZMod 41 × ZMod 41 // xy.2 ^ 2 + xy.2 = xy.1 ^ 5} + 1 = 33 ∧
    Nat.card {xy : GaloisField 41 2 × GaloisField 41 2 // xy.2 ^ 2 + xy.2 = xy.1 ^ 5} + 1 = 1743 := 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" (counting yields

N_1=33

and

N_2=1743

)

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

y2+y=x5y^2+y=x^5y2+y=x5 over F41\mathbb F_{41}F41​: N1=33N_1=33N1​=33, N2=1743N_2=1743N2​=1743

$y^2+y=x^5$ over $\mathbb F_{41}$ : $N_1=33$ , $N_2=1743$