AI Proof WatchKeep up with AI contributions

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

For every numerical semigroup S and integer p≥0, AxiomProver’s Lean proof establishes Fel’s formula for the normalized alternating syzygy quantity Kₚ(S) in terms of universal symmetric polynomials, gap power sums and a final polynomial term.

Sources for this record

What was already known

Fel proposed this numerical-semigroup syzygy identity as a conjecture. Related universal-polynomial identities had been proved by human researchers, but did not settle Fel’s Kₚ(S) formula.

AI involvement AI-autonomous

AxiomProver received a self-contained problem statement and a one-line request to state and prove it in Lean, then generated the formal statement and complete proof. Human authors chose the target and later wrote a separate explanatory derivation.

The documented run supplied only a specified problem and environment; AxiomProver generated the theorem statement and proof without human mathematical hints after the task was set.

Importance Notable

The formal theorem resolves the remaining identity for all numerical semigroups and all p≥0.

Limitations

The reported proof uses Lean 4.26.0. The repository’s later main branch names a different toolchain, so it should not be treated as the exact paper run.

Technical verification Formal (Lean 4/Mathlib kernel verification of the formal theorem)

The paper reports a complete Lean/Mathlib proof of Fel's exact formula generated from the natural-language target. The repository supplies problem and solution files and Comparator instructions. This supports a source-reported machine check of the stated identity, while the live repository's later toolchain differs from the paper's documented Lean 4.26.0 run.

Formal checking

Complete Lean/Mathlib proof generated from problem.lean and checked under the paper's Lean 4.26.0 environment

Checker
Lean 4 kernel in AxiomProver's reported run
Scope
The formalized Fel Conjecture 1.6 identity for every numerical semigroup and p ≥ 0
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

The human authors explicitly wrote a self-contained formal-power-series derivation and explanatory paper after the Lean result, identifying the coefficient extraction that proves the same formula.

Correction and publication history