math.AG — Algebraic Geometry
Contributed by Johannes Schmitt
Chen and Larson study tautological classes on the strata of holomorphic
abelian differentials, where they predict a vanishing result. Using known
tautological relations on the moduli space of curves, they reduce this
prediction to the non-vanishing of certain coefficients of a quotient of
hypergeometric generating series, treating the residue classes
g≡0,2(mod3) and g≡1(mod3) through two separate series; they verify
the non-vanishing by computer for small genus.
We prove it in general: in both cases the relevant coefficient is non-vanishing
for every genus and every stratum, and in the first case it has, more strongly,
a uniform strict sign. Along the way we correct an error in the Chen--Larson
derivation of the g≡1(mod3) series, where a constant of the underlying
relation of Ionel had inadvertently been changed.
The paper falls into two parts. Part~I gives the mathematical proofs; Part~II
documents the Lean~4 and Mathlib formalization --- whose only non-standard trust
assumption is the compiler invoked by \code{native\_decide} for the large finite
computations --- together with the long-horizon, multi-model generative-AI
process that produced the proofs, exposed false intermediate routes, and
uncovered the error in the printed Proposition~5.2 relation noted above.
Primarily AI-generated textHuman understanding: not declaredpower seriestautological classes