HEXAGONbeta

Strict negativity and non-vanishing of Chen--Larson hypergeometric coefficients

Primarily AI-generated textHuman understanding: not declaredmath.AG — Algebraic Geometrycs.AI — Artificial Intelligencemath.AC — Commutative Algebra

Contributed by Johannes Schmitt ↗

SubmitterJohannes Schmitt

Version 1 / Sep 01, 2026 / CC BY 4.0

Abstract

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)g\equiv0,2\pmod3 and g≡1(mod3)g\equiv1\pmod3 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)g\equiv1\pmod3 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.

Provenance statement

The mathematical content and the Lean 4 formalization of this paper were generated by general-purpose AI systems within a human-orchestrated, multi-model workflow; the author's role was orchestration, not mathematical authorship. Systems used: ChatGPT 5.5 Pro (central research strand, adversarial paragraph-level audits of notes and code, strategic reviews, the Proposition 5.2 proof and the audit that found the error in the printed relation, expository draft); Claude Fable 5 (strategic guidance; first Lean formalization push via Claude Code); Claude Opus 4.8 (reviews run in parallel with ChatGPT 5.5 Pro); OpenAI Codex CLI (long-horizon Lean completion under a persistent /goal); Claude Code (manuscript revisions). Degree of autonomy: Level A in the classification of Feng et al. (arXiv:2602.10177): the author did not originate or modify any lemma, estimate, proof strategy or Lean proof. The Prop. 5.1 formalization ran as one Codex goal thread (about 64 h elapsed, 15-20 June 2026) and needed one mid-run redirection; the diagnosis, that the worker was pursuing a provably false product estimate, came from AI reviews and was relayed to the worker unaltered. The Prop. 5.2 formalization was completed by a fresh Codex worker from an AI-authored plan in about 20 h with no mathematical or technical intervention. No theorem-level claim was accepted on a model's assertion; acceptance rested on a Lean proof or an independently checked derivation. Tools: Lean 4.27.0 with a pinned Mathlib revision. Large finite certificates (partition enumeration, exact rationals, 192-bit dyadic intervals, modular checks) are executed by native_decide, which adds the axioms Lean.ofReduceBool and Lean.trustCompiler to propext, Classical.choice and Quot.sound; no sorry and no project-specific axioms (audit: scripts/PublicAxiomsReport.lean; lean4checker replays the non-native proofs). AI-written Python scripts and Arb ball arithmetic were used during discovery only. Human interventions: problem selection (after H. Larson's ETH Zurich talk, 10 June 2026); prompt design and routing between independent conversations; maintenance of the computational and Lean environment; judging from high-level progress signals when the autonomous worker had stalled and escalating its own blocking questions to fresh reviews; relaying the AI-audit finding that the constant kappa_0 = 2g-2 of Ionel's relation appears as 1 in the printed Chen-Larson Proposition 5.2 (confirmed by the authors, June 2026); curation of the provenance record; direction, editorial judgement and final responsibility for the manuscript, whose text was itself AI-drafted and AI-revised. Available traces: seven human-AI interaction cards with verbatim or closely paraphrased prompts (Part II of the paper), linked to public shared conversations where they exist; curated, redacted records of the command-line-agent sessions (every on-topic human instruction, AI side summarized) and the key review exchanges under docs/ai-correspondence/ in the tagged repository release, together with certificate-generation provenance and the one-command axiom audit. Token counts, monetary cost and human active time were not recorded.

Tools used

OpenAI
GPT-5.5 Pro
OpenAI
codex CLI
Anthropic
Claude Opus 4.8
Anthropic
Claude Fable 5

References

  1. D. Chen and H. Larson, Independence of tautological classes and cohomological stability for strata of differentials , arXiv:2603.23850v1, 25 March 2026 (Proposition 5.2 and equation (5.4)).arXiv
  2. E.-N. Ionel, Relations in the tautological ring of $ M_g$ , Duke Math. J. 129 (2005), no. 1, 157--186; arXiv:math/0312100 (Proposition 1.7, equation (1.13)).arXiv
  3. The Lean development team, Lean Reference Manual: Axioms and validating proofs , https://lean-lang.org/doc/reference/latest/Axioms/ , accessed June 2026.link
  4. The Mathlib community, Mathlib: the mathematical library for Lean 4 , https://github.com/leanprover-community/mathlib4 .link
  5. T. Feng et al., Towards Autonomous Mathematics Research , arXiv:2602.10177, 2026.arXiv
  6. R. Pathak and S. Fabbri, Using Goals in Codex , OpenAI Developers, 9 May 2026, https://developers.openai.com/cookbook/examples/codex/using_goals_in_codex , accessed June 2026.link
  7. arXiv:2603.23850arXiv

Version history

  1. v1Revised after moderator-requested changesCurrentSep 01, 2026