← All papers
Parity of $k$-differentials in genus zero and one
math.NT
Feb 3, 2026 · v1
TL;DR
AxiomProver formalized the proof of a combinatorial identity in Lean/Mathlib for the spin-parity result.
Abstract
Here we completely determine the spin parity of $k$-differentials with prescribed zero and pole orders on Riemann surfaces of genus zero and one. This result was previously obtained conditionally by the first author and Quentin Gendron assuming the truth of a number-theoretic hypothesis Conjecture A.10. We prove this hypothesis by reformulating it in terms of Jacobi symbols, reducing the proof to a combinatorial identity and standard facts about Jacobi symbols. The proof was obtained by AxiomProver and the system formalized the proof of the combinatorial identity in Lean/Mathlib (see the Appendix).
Problem
The spin parity of k-differentials with prescribed zero and pole orders on Riemann surfaces of genus zero and one was determined only conditionally, assuming an unproven number-theoretic hypothesis (Conjecture A.10).
Approach
The authors prove Conjecture A.10 by reformulating it in terms of Jacobi symbols, reducing the proof to a combinatorial identity and standard facts about Jacobi symbols. The key reformulation was discovered by AxiomProver, an AI proof system, and the combinatorial identity was formalized in Lean/Mathlib.
Results
The spin parity of k-differentials in genus zero and one is now unconditionally determined. The Lean formalization verifies the combinatorial identity that constitutes the key technical step.