Fel's Conjecture on Syzygies of Numerical Semigroups

Let $S=⟨d_1,\dots ,d_m⟩$ 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\mathrm{\notin }S}{g}^r$ and universal symmetric polynomials $T_n$ evaluated at the generator power sums ${\sigma }_k={\sum }_i{d}_i^k$ (and ${\delta }_k=({\sigma }_k-1)\mathrm{/}{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.