We used Fel’s conjecture on numerical semigroups as a stress test for the automated reasoning system we’re developing. Axiom Prover autonomously assembled a proof formally verified in Lean, validating a solution that offers an unexpected connection to identities in Ramanujan’s century-old Lost Notebook.
Recent progress in AI-driven problem solving has been striking, especially in competition-style mathematics, where problems are self-contained, techniques are well-trodden, and solutions tend to be short. That’s exciting, but it’s not the same thing as doing mathematics research.
Research lives in a different regime. The problem statement is often inseparable from surrounding definitions, notation, and context. Proofs can be long chains of dependent lemmas. The space of plausible next steps is enormous, and novelty matters. Most importantly, correctness is not optional: a convincing research proof isn’t just an answer, it’s an artifact the community can scrutinize and build on.
Axiom’s mission is to bring AI into this research regime by pairing powerful generative methods with formal verification. The north star is not merely getting to the right idea, but producing results that can be checked down to the last inference.
To that end, we are building an in-house system we call Axiom Prover. Given a conjecture written in natural mathematical language together with the relevant definitions, it generates a proof in a form that can be formally verified in Lean/Mathlib. The proof is only accepted once the checker accepts it.
As an early test case, and a case study in what this workflow looks like in practice, we posed to Axiom Prover an open conjecture of Fel about syzygy invariants of numerical semigroups. What follows is the story of that experiment, what the system produced, and what we learned.
This post accompanies the arXiv preprint of our paper, Fel’s Conjecture on Syzygies of Numerical Semigroups, which proves an explicit closed formula for normalized syzygy invariants of numerical semigroups. It also serves as an early case study for Axiom Prover: starting from a natural-language statement of the conjecture together with a small package of formal definitions, the system autonomously assembled a proof and produced a Lean/Mathlib proof artifact that the checker accepts.
Zero human involvement (transparency). After kickoff, we did not steer the prover with hints, add helper lemmas by hand, or patch the Lean proof manually. Axiom Prover generated the intermediate lemmas and the final Lean/Mathlib proof artifact, and the proof is accepted only because Lean’s checker accepts it (see discussion below).
Scope note: This post is a case study in a particular workflow, not a sweeping claim about automating research. What makes it interesting to us is the form of the output, an independently checkable Lean/Mathlib proof artifact, so the reliability comes from formal verification rather than from the model’s own explanations.
We give a brief mathematical overview, work through concrete examples, and then describe the end-to-end pipeline that turns a research conjecture into a verified proof. For transparency, we describe below exactly what was provided by us and what was generated by the system (lemmas, proof structure, and the final Lean proof term).
Why Fel’s conjecture?
We wanted a test case that was genuinely open in the research literature, but still close enough to existing theory that a clean closed-form answer ought to exist. To stress-test Axiom Prover, we deliberately chose a problem with these features:
Open and nontrivial: Fel’s conjecture was unresolved, and settling it requires real algebra, not just a clever one-liner.
Feasible to formalize today: We expected the argument could avoid a full formal build-out of numerical semigroups, minimal resolutions, and symmetric-function machinery, so a Lean/Mathlib verification was realistic.
Mathematically central: It sits at the intersection of additive number theory, commutative algebra, and the study of Hilbert series and syzygies.
Structured enough for a closed form: Rigid enough that a clean formula should exist, but still with enough moving parts to demand careful manipulation and bookkeeping.
Timely: The $T_n$ polynomials have gained renewed relevance in connection with Ramanujan’s Lost Notebook and quasimodular forms (see this paper by Amdeberhan, Fel, and Ono). In his own handwriting, we share the definition of two strange sequences of power series Ramanujan recorded in his Lost Notebook:
There is a convenient way of repackaging Ramanujan’s series that gives auxiliary functions
\[\tilde{Y}_n(x) := \frac{1}{(n+1)2^{n}} \sum_{k=0}^{\left[\frac{n}{2}\right]} \binom{n+1}{2k+1}\, p_1(x)^{\,n-2k}\cdot \Psi\!\bigl(U_{2k}(q)\bigr).\]
which Amdeberhan et al. prove coincide with the $T_n$ polynomials.
Theorem 1.3. For every pair of positive integers $k$ and $n$, we have $\tilde{Y}_n\!\left(x^{k}\right) = T_n\!\left(x^{k}\right)$
From conjecture to certified proof. In this case study, Axiom Prover went end-to-end: it translated the conjecture into a precise formal target, autonomously assembled a proof plan consisting of supporting lemmas, and produced a Lean/Mathlib proof artifact that the kernel accepts. The headline isn’t just that a proof was found; it’s that the result is a checkable object others can inspect, rerun, and build on.
The mathematical setting in a nutshell
A numerical semigroup is a set of nonnegative integers closed under addition with finite complement in $\mathbb{N}$. Concretely, it is typically given by generators:
\[S := \langle d_1, \ldots, d_m \rangle \subseteq \mathbb{Z}_{\ge 0}\]
The missing numbers (the gaps) form a finite set $\Delta = \mathbb{N} \setminus S$. In recreational math, this is often called the Coin Problem or Frobenius Coin Problem: given coins of denominations $d_1, \ldots, d_m$, what is the largest amount you cannot make change for?
A simple way to package the gaps is via their power sums. For each non-negative integer $r$ define:
\[G_r(S) := \sum_{g \in \Delta} g^{r}\]
Numerical semigroups connect additive number theory with commutative algebra through the semigroup ring $k[S]$. One studies $k[S]$ via its Hilbert series, a generating function that counts degrees:
\[H_S(z) := \sum_{s \in S} z^{s}\]
which can be expressed as a rational function
\[H_S(z) = \frac{Q_S(z)}{\prod_{i=1}^{m} \left(1 - z^{d_i}\right)}\]
It is a rational function whose denominator is determined by the generators $d_i$ and whose numerator encodes subtle algebraic information. It controls the degrees of the syzygies appearing in a minimal free resolution of $k[S]$.
Very roughly, syzygies measure relations among relations, the hidden constraints that show up after you’ve already written down the obvious equations. If you like the astronomer’s use of the word, think of a syzygy as an alignment: not planets lining up in the sky, but algebraic dependencies lining up behind the scenes. They’re core invariants in commutative algebra and algebraic geometry, and in the numerical semigroup world they plug directly into the toric/monomial toolkit that makes these problems computable and surprisingly rigid.
Fel introduced alternating power-sum invariants extracted from the Hilbert series, and then defined normalized combinations $K_p(S)$ that are designed to have a clean, generator-independent description.
The universal symmetric polynomials Tₙ and Ramanujan’s Lost Notebook
Fel’s conjecture involves a family of universal symmetric polynomials $T_0, T_1, T_2, \ldots$. These are symmetric polynomials in variables $x_1, x_2, \ldots$ defined by a generating function, and they can be evaluated on the power sums of the generators $d_i$. In our setting we use the sequences:
\[\sigma_k := \sum_{i=1}^{m} d_i^{k} \quad \text{and} \quad \delta_k := \frac{\sigma_k - 1}{2^{k}}.\]
These $T_n$ are interesting well beyond numerical semigroups. They also appear in problems about restricted partitions and, strikingly, in the theory of quasimodular forms connected to Ramanujan’s work.
In his Lost Notebook (circa 1920), Ramanujan defined a family of q-series $U_{2n} (q)$ arising from derivatives of Jacobi’s theta function and conjectured deep modularity properties. A century later, these series are still yielding new structure. Recent work of Amdeberhan, Fel, and Ono shows that the same universal polynomials $T_n$ arise naturally as symmetric-function avatars of quasimodular forms built from Ramanujan’s $U_{2n} (q)$. This connection was used to settle conjectures about the $T_n$ and to clarify the structure behind Ramanujan’s series.
Two examples of Fel’s formula
Fel’s conjecture gives a uniform expression for Kₚ(S) for every numerical semigroup S. Here are two concrete examples (both appear in the paper).
Example 1: S = ⟨3, 5⟩
The gap set is $\Delta = \{1, 2, 4, 7\}$. The Hilbert numerator is $1 - z^{15}$, and the resulting normalized invariant is:
\[K_p(S) = \frac{15^{p+1}}{(p+1)(p+2)}.\]
Example 2: S = ⟨4, 5, 6⟩
The gap set is $\Delta = \{1, 2, 3, 7\}$. The Hilbert numerator is $1 - z^{10} - z^{12} + z^{22}$, and one obtains:
\[K_p(S) = \frac{22^{p+3} - 10^{p+3} - 12^{p+3}}{120(p+1)(p+2)(p+3)}.\]
Even in these small cases, it is not obvious a priori that such clean expressions for all $p$ should exist. Fel’s conjecture predicts that this phenomenon holds in complete generality, governed by the gap power sums $G_r(S)$ and the universal polynomials $T_n$.
Fel’s Conjecture and the main theorem
Let $S = \langle d_1, \ldots, d_m \rangle$ be a numerical semigroup and let $\Delta = \mathbb{N} \setminus S$ be its gap set. We let $T_n(\sigma)$ and $T_n (\delta)$ be the universal symmetric polynomials evaluated at $(\sigma_1, \sigma_2, \ldots)$ and ($(\delta_1, \delta_2, \ldots)$.
Fel’s conjecture is a closed formula for the normalized syzygy invariants $K_p (S)$:
Conjecture (Fel). For every integer $p \geq 0$, we have
$K_p(S) = \sum_{r=0}^{p} \binom{p}{r} \, T_{p-r}(\sigma)\, G_r(S) \;+\; \frac{2^{p+1}}{p+1}\, T_{p+1}(\delta)$
Theorem. Fel’s Conjecture is true. (Proof generated by Axiom Prover; verified in Lean/Mathlib.)
In other words: Axiom Prover gives a generator-independent closed formula for $K_p(S)$. It is determined explicitly by the combinatorics of the gaps (the numbers missing from $S$) and by the universal polynomials $T_n$, with no additional semigroup-specific input.
The proof idea. The proof hinges on the change of variables $z = e^t$ and a systematic use of exponential generating functions. With that viewpoint, the Hilbert-series algebra turns into a set of clean pick out the right coefficient statements. But it doesn’t boil down to a one-liner like many competition problems. In this work there’s real infrastructure to build, intermediate identities, careful expansions, and a lot of bookkeeping to keep the coefficients straight. Universal identities for the polynomials $T_n$ supply the key inputs that ultimately let us isolate the specific coefficient encoding $K_p(S)$.
How Axiom Prover produced the proof
We describe the workflow, with links for those who want to dive into the details.
1. The Inputs (Natural-language statement)
We provided Axiom Prover with a natural-language formulation of Fel’s conjecture together with a self-contained list of definitions (numerical semigroup, gap set, Hilbert series numerator, the invariants $K_p (S)$, and the defining properties of $T_n$). Here are the files:
Fel_conjecture.tex: a LaTeX file containing the statement of the conjecture.task.md: a file containing one sentence: 1. State and prove Fel’s conjecture in Lean..
.environment: a file specifying the version of Lean and Mathlib: 4.26.0.
2. Autoformalization in Lean
AxiomProver translated the informal statement found in the LaTeX file into Lean 4.26.0, reusing Mathlib’s infrastructure for formal power series, algebra, and combinatorics. Here is the output file:
problem.lean: a formal statement of the conjecture in Lean.
3. Automated lemma proving and bookkeeping
AxiomProver generated the required intermediate lemmas (about series expansions, products, and coefficient operators) and chained them together into a complete argument, with Lean checking every step. Here is the output file:
solution.lean: a formal proof of the conjecture in Lean.
4. Artifacts
arXiv paper written by humans https://arxiv.org/abs/2602.03716,
GitHub repo. https://github.com/AxiomMath/fel-polynomial/
What we learned
This test case worked beautifully: once the definitions were in place, the path from a clean mathematical statement to a mechanically checked proof was smoother than we expected. It also reinforced a simple point: the limiting factor is rarely AI in the abstract. It’s the quality and breadth of the shared library it can build on. Mathlib is already an extraordinary public good, and every new lemma, abstraction, and refactor compounds in value by making the next formalization cheaper, faster, and more reliable. We hope this encourages more mathematicians to contribute: not because formalization is a side quest, but because we increasingly believe it is where the future of mathematics is headed. For our part, this success has us excited to keep pushing—more theorems, more formalization, and more fun along the way.