PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2602.03716v2math.COmath.ACmath.NT

TL;DR

Fel formulated Conjecture 1.6 for every p ≥ 0. The proof uses exponential generating functions and coefficient extraction, with the resulting argument formalized in Lean/Mathlib. Fel’s conjecture is proved for every p ≥ 0, and the paper records T_n identities relating restricted partitions and Ramanujan’s q-series.

  • Problem

    Fel formulated Conjecture 1.6 for every p ≥ 0.

    Source: §1.2 · p. 3

  • Method

    The proof uses exponential generating functions and coefficient extraction, with the resulting argument formalized in Lean/Mathlib.

    Source: §1 · p. 2, §1.4 · p. 5

  • Results

    Fel’s conjecture is proved for every p ≥ 0, and the paper records T_n identities relating restricted partitions and Ramanujan’s q-series.

    Source: §1.3.1 · p. 4, §1.4 · p. 5, §1.3.3 · p. 5

  • Takeaways & Limitations

    The work resolves the remaining conjecture about K_p(S) and supplies a fully verified automated-proof case study.

    Source: §1.4 · p. 5

    The Hilbert-numerator setup notes additional constraints on partial Betti numbers and syzygy degrees, but does not need them for the subsequent definition.

    Source: §1.1 · p. 2

Abstract

from arXiv · show

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 $\sigma_k=\sum_i d_i^k$ (and $\delta_k=(\sigma_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.

1. Introduction

The paper places Fel’s conjecture in the study of numerical semigroups, Hilbert numerators, syzygy degrees, and universal symmetric polynomials, then proves the conjecture for every p using formal power series. It also records connections between the polynomials T_n and restricted partitions, zig-zag recursions, and Ramanujan’s q-series before presenting a Lean/Mathlib formalization.

1.2. Fel’s sequence Tn of universal symmetric polynomials.

  • Fel’s conjecture expresses K_p(S) using gap power sums G_r and universal symmetric polynomials T_n evaluated on generator power sums.The polynomials T_n are introduced as the universal objects governing the K_p formulas.Source: §1 · p. 2, §1.2 · p. 3

1.4. Main result.

  • The proof converts semigroup, gap, and coefficient data into exponential generating functions and derives the result by formal algebra and coefficient extraction.The strategy replaces ordinary-generating-function variables with exponential ones whenever possible.Source: §1 · p. 2, §1.4 · p. 5

1.1. Hilbert series of numerical semigroups, and alternating syzygy.

  • The Hilbert numerator of k[S] encodes syzygy degrees through an alternating sum, whose alternating power sums lead to the coefficients K_p(S).The Hilbert series has a polynomial numerator, and its monomial degrees are the syzygy degrees used in the alternating power sums.Source: §1.1 · p. 2

1.3. The reappearance of Tn in relation to Ramanujan’s U2n(q) and other contexts.

  • The paper situates T_n in broader mathematics through restricted partitions, zig-zag-number recursions, and Ramanujan’s q-series, while noting these contexts are not used in the main proof.The q-series construction gives symmetric-function avatars satisfying T_n(x_1, …, x_k) = eY_n(x_1, …, x_k, 0, …), and this interpretation supports the restricted-partition and recursion results.Source: §1.3 · p. 3, §1.3.2 · p. 4, §1.3.3 · p. 5

1.3.1. Restricted partitions.

  • For restricted partitions, the coefficients f_n are identified with T_n after sign changes in the generator power sums.The stated identity is f_n(σ_1, …, σ_n) = T_n(σ_1, −σ_2, …, −σ_n).Source: §1.3.1 · p. 4

1.4. Main result.

  • The paper proves Fel’s conjecture for every p ≥ 0, giving the conjectured formula for normalized syzygy power-sum coefficients K_p(S).The main theorem states that Conjecture 1.6 is true for all p.Source: §1 · p. 2, §1.2 · p. 3, §1.4 · p. 5
  • The result was generated and fully verified in Lean/Mathlib by AxiomProver from a natural-language formulation of the conjecture.The exposition is presented as a case study in end-to-end automated theorem proving.Source: §1.4 · p. 5

appendix.)

The authors acknowledge discussions with Tewodros Amdeberhan and Leonid Fel, along with helpful corrections from anonymous referees.

  • The paper thanks Tewodros Amdeberhan and Leonid Fel for discussions and anonymous referees for helpful corrections.Source: §1.5 · p. 5

2. Background

The background establishes the syzygy-degree quantities and develops universal symmetric polynomials through exponential generating functions, first in generator variables and then in power-sum coordinates.

2.1. Syzygy degrees.

  • The section recalls Kp(S), the Hilbert-series numerator QS(z), and coefficients used to express syzygy-related quantities.The definition is described as sufficient for proving Theorem 1.11 despite not directly using partial Betti numbers.Source: §2.1 · pp. 5–6

2.2. Universal symmetric polynomials, in terms of xi.

  • The universal polynomials Tn are recast from Fel’s original definition [Fel21, §2] using an exponential generating function A(t).Coefficient extraction from A(t) recovers the original definition.Source: §2.2 · p. 6

2.3. Universal symmetric polynomials, in terms of σk.

  • Tn is symmetric and homogeneous of degree n, so the paper rewrites it in the power-sum basis σk, suppressing explicit dependence on m.Examples through n ≤ 7 are recorded later.Source: §2.3 · p. 7

2.4. Universal symmetric polynomials, in terms of δk.

  • Replacing σk with δk yields the scaling identity Tn(δ) = 1 2^n Tn(σ −1).The transformed generating function is B(t) := t/(e^t−1) A(t).Source: §2.4 · p. 7

3. Worked examples

Worked examples list explicit Tn formulas and instantiate the Hilbert-series, gap, generator, and syzygy calculations for three numerical semigroups.

3. Worked examples

  • The examples provide Tn in the σk basis through n ≤ 7, then compute Δ, Gr, σk, δk, Cn, and Kp for selected semigroups.The examples are presented as reference material and may be skipped without loss of continuity.Source: §3 · p. 8, §3.1 · p. 8

3.2. Worked example S = ⟨3, 5⟩.

  • For S = ⟨3, 5⟩, the Hilbert numerator is QS(z) = 1 − z^15, yielding Kp(S) through C2+p(S) and the factor (p + 1)(p + 2).Source: §3.2 · pp. 8–9

3.3. Worked example S = ⟨4, 5, 6⟩.

  • For S = ⟨4, 5, 6⟩, the Hilbert numerator is QS(z) = 1 − z^10 − z^12 + z^22, yielding Kp(S) with denominator 120(p + 1)(p + 2)(p + 3).The result also follows from [Fel22, equation (63)] because the semigroup is a symmetric complete intersection.Source: §3.3 · p. 9

3.4. Worked example S = ⟨5, 6, 8, 9⟩.

  • For S = ⟨5, 6, 8, 9⟩, the gap set is Δ = {1, 2, 3, 4, 7}, and the computed syzygy expression is Kp(S) = Cp+4(S) / [2160(p + 1)(p + 2)(p + 3)(p + 4)].The example also records the Hilbert-series numerator and an explicit expression for Cn(S).Source: §3.4 · pp. 9–10

4. Proof of Theorem 1.11

The proof converts the gap and syzygy data into exponential generating functions, substitutes z = e^t, and extracts coefficients to establish Fel’s conjectured identity.

  • The proof strategy replaces ordinary generating-function expressions in z with exponential generating functions in t, translating both Gr(S) and Cr(S).The conversion uses the Hilbert-series numerator, the product polynomial, and the auxiliary generating functions A(t) and B(t).Source: §4 · pp. 10–11
  • The Hilbert-series relation ΦS(z) = 1/(1 − z) − HS(z) is combined with z = e^t to connect the gap generating function with the polynomial framework.Source: §4 · p. 11
  • Choosing n = m + p and comparing the t^(m+p) coefficients combines the generating-function identities needed for the conjectured formula.The coefficient comparison is completed after multiplying by p!.Source: §4 · p. 12
  • The final coefficient identity gives Conjecture 1.6 and completes the proof of Theorem 1.11.Source: §4 · p. 12

Appendix

The paper presents Fel’s conjecture as an end-to-end formalization target for AxiomProver and reports a fully verified Lean/Mathlib proof produced from a natural-language statement.

Appendix

  • AxiomProver was selected because the conjecture appeared formalizable without fully developing numerical semigroups, resolutions, and symmetric functions.The choice also reflected renewed interest in the universal polynomials T_n.Source: Appendix · p. 12
  • The formal statement and proof were produced by AxiomProver and fully formalized in Lean/Mathlib.Source: Appendix · p. 13
  • The formal proofs were developed and verified using Lean 4.26.0, with compatibility with other versions not guaranteed.Source: Process · p. 13

Process.

The process begins with a natural-language conjecture and a minimal task specification, after which AxiomProver generates complete Lean formalizations; the authors then write a human-oriented exposition.

Process.

  • The repository input consisted of a natural-language problem statement, a one-line task to state and prove Fel’s conjecture, and a Lean-version configuration.Source: Process · p. 13
  • AxiomProver generated Lean files containing the formalized problem statement and a complete formalized proof.Source: Process · p. 13
  • The examples file was handwritten and separate from the formalization inputs provided to AxiomProver.Source: Process · p. 13
  • After generation, the human authors wrote the paper for readers because research exposition and Lean files serve different purposes.Source: Process · p. 13

Further commentary.

The commentary frames the work as an early end-to-end formalization of research mathematics and explains that the problem was chosen to fit current Mathlib capabilities.

Further commentary.

  • This work is presented as an early example of an AI system solving and verifying a research-mathematics problem end to end.Source: Further commentary · p. 13
  • The authors deliberately selected an open problem believed to be within reach of the current Mathlib repository.Source: Further commentary · p. 13
  • Avoiding gaps in Mathlib was an explicit selection criterion for the formalization target.Source: Further commentary · p. 13
Loading 2602.03716v2…