Parity of $k$-differentials in genus zero and one

Dawei Chen, Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang

math.NT Feb 3, 2026 · v2 math.AG math.GT

formalization ai-agents number-theory mathlib

Read PDF arXiv abstract Code

TL;DR

AxiomProver autonomously produced Lean 4.26.0/Mathlib formalizations of the problem statement and a key combinatorial floor-sum identity, posted on GitHub.

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

Determining the spin parity of k-differentials with prescribed zero and pole orders on genus zero and one Riemann surfaces had been reduced to a number-theoretic hypothesis (Conjecture A.10 of Chen–Gendron) that remained unproven.

Approach

The conjecture is reformulated using Jacobi symbols, exploiting that floor((k+1)/4) mod 2 is periodic modulo 8 and matches the symbol (2/k). Via the Eisenstein and Gauss–Schering lemmas and the supplementary law, the proof reduces to an explicit combinatorial floor-sum identity (Lemma 2.5). AxiomProver, an AI system, was given only the conjecture statement and found this reformulation. It then autonomously produced Lean 4 files formalizing the statement and proof of Lemma 2.5.

Results

The conjecture is proved, which completely determines the spin parity of k-differentials in genus zero and one. The Lean proof of the combinatorial identity is verified, and it shows that an assumed gcd hypothesis is unnecessary.

Papers With

Parity of $k$-differentials in genus zero and one