Fel's Conjecture on Syzygies of Numerical Semigroups
Evan Chen, Chris Cummins, GSM, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian Zhang
math.CO
Feb 3, 2026 · v1
TL;DR
Proof of Fel's conjecture on numerical-semigroup syzygies formalized in Lean/Mathlib via AxiomProver.
Abstract
Let $S=\langle d_1,\dots,d_m\rangle$ be a numerical semigroup and $k[S]$ its semigroup ring. The Hilbert numerator of $k[S]$ determines normalized alternating syzygy power sums $K_p(S)$ encoding alternating power sums of syzygy degrees. Fel conjectured an explicit formula for $K_p(S)$, for all $p\ge 0$, in terms of the gap power sums $G_r(S)=\sum_{g\notin S} g^r$ and universal symmetric polynomials $T_n$ evaluated at the generator power sums $σ_k=\sum_i d_i^k$ (and $δ_k=(σ_k-1)/2^k$). We prove Fel's conjecture via exponential generating functions and coefficient extraction, solating the universal identities for $T_n$ needed for the derivation. The argument is fully formalized in Lean/Mathlib, and was produced automatically by AxiomProver from a natural-language statement of the conjecture.
Problem
Fel conjectured an explicit formula for normalized alternating syzygy power sums K_p(S) of numerical semigroups in terms of gap power sums and universal symmetric polynomials evaluated at generator power sums. The conjecture remained unproven.
Approach
The proof proceeds via exponential generating functions and coefficient extraction, isolating the universal symmetric polynomials T_n as coefficients of an explicit generating series. The authors verify the conjecture and provide a partial Lean formalization covering the algebraic identities and key combinatorial steps.
Results
Fel's conjecture is proved for all p >= 0 and all numerical semigroups. The formula expresses K_p(S) in terms of gap power sums G_r(S) and the universal polynomials T_n evaluated at generator power sums. Worked examples for specific semigroups confirm the formula.
