Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Fermat certificates for every homogeneous odd source

Proved
HodgeComputer.Fermat.certificate

by benediamond · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryfermathodge-computer

For each q∈{1,2}q\in\{1,2\}q∈{1,2} and every homogeneous polynomial A∈C[X0,X1,X2,Y0,Y1,Y2]A\in\mathbb C[X_0,X_1,X_2,Y_0,Y_1,Y_2]A∈C[X0​,X1​,X2​,Y0​,Y1​,Y2​] of degree 6⋅q6\cdot q6⋅q satisfying A(X,−Y)=−A(X,Y)A(X,-Y)=-A(X,Y)A(X,−Y)=−A(X,Y), the Fermat sextic F=∑i=02(Xi6+Yi6)F=\sum_{i=0}^{2}(X_i^6+Y_i^6)F=∑i=02​(Xi6​+Yi6​) admits a Diamond certificate: a rational vector field vvv homogeneous of degree 6⋅q−56\cdot q-56⋅q−5, with common denominator relatively prime to FFF, satisfying Fq+1∣A−q⋅dF(v)+F⋅div⁡(v)F^{q+1}\mid A-q\cdot dF(v)+F\cdot\operatorname{div}(v)Fq+1∣A−q⋅dF(v)+F⋅div(v). Divisibility is in the localization with denominators relatively prime to FFF; there is no bound on denominator degree.

Preamble
import Definitions.Def_HodgeComputerFermat
Formal statement
theorem HodgeComputer.Fermat.certificate
    (q : ℕ) (hq : q = 1 ∨ q = 2)
    (A : HodgeComputer.AmbientPoly HodgeComputer.Fermat.n)
    (hA : A.IsHomogeneous (HodgeComputer.Fermat.d * q))
    (hodd : HodgeComputer.Fermat.OddSource A) :
    HodgeComputer.HasCertificate
      HodgeComputer.Fermat.F
      A
      HodgeComputer.Fermat.d
      q := by
  sorry
Source
Benjamin E. Diamond, Hodge Structures in Sextic Fourfolds Equipped with an Involution, https://arxiv.org/abs/2603.29157, Section 3; subset Euler construction specialized to the sign-flip involution. Formalization: https://github.com/hodge-computer/sextics/blob/39daa1c576de10ace509adb1faa500080a5619a9/formal/lean/HodgeComputer/Constructions/Fermat.lean (site counterpart with inferred degree).

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