Rogers–Ramanujan for every a, b?

The claim, in plain words

This is AX03, about a paper from Axiom Math and Emory University. Write the number six as a sum of parts that differ by at least two: six, five plus one, four plus two. That makes three ways. Now write six using only parts that leave remainder one or four when divided by five: six, four plus one plus one, and six ones. Again, three. Our computer finds the two counts equal for every number up to 40, and the first Rogers–Ramanujan identity says they are always equal. In formulas, a sum of q^(n²) over a product equals an infinite product over the residues one and four, modulo five. The paper cites Rogers’s memoir of 1894. Gordon’s partition theorem and Andrews’s identities extend the modulus five to every odd modulus. A quadratic sum equal to a product with congruence conditions: that is the shape this paper generalizes.

Where could such identities come from? Huang, Jiang and Oblomkov proposed a geometric source. Take two n × n matrices, A and B, over a finite field with q elements. Ask that both are nilpotent, meaning some power is zero, that they commute, and that A^a = B^b, for coprime numbers a and b. Over the field with two elements, with a equal to three and b equal to four, our count finds one such pair of 1 × 1 matrices, ten pairs of 2 × 2 matrices, and 400 of 3 × 3. What organizes these counts are the gaps: the numbers you cannot write as a sum of threes and fours. Here they are one, two and five. The counts are assembled, by a theorem of Huang, Jiang and Oblomkov, into a q-series, Z, with one summation variable for each gap, and the conjecture says Z equals an explicit infinite product, P, whose exponents repeat modulo a plus b. For a equal to two, the gaps form a chain, and the conjecture is exactly one family of the Andrews–Gordon identities. For three and four, they do not, and the product has modulus seven.

Episode AX03 covers one preprint on the arXiv, 38 pages, titled Rogers–Ramanujan identities from the geometry of X^a = Y^b. Its authors are Yifeng Huang of Emory University, and Kenny Lau and Ken Ono of Axiom Math. Version one is dated September 17, 2026, and version two October 7. The paper says that apart from a equal to two, little was known: four cases with a equal to three, in an earlier paper by the same authors with Peter Paule, and then all of a equal to three, by Lau and Ono. Nothing was known for a above three. The claim is that the conjecture holds for every coprime pair, with a less than b. The main theorem is a stronger finite identity. Take the finite sum at rank N, and it equals a product of N simple factors times the generating function for balanced cylindric partitions: a rows of numbers that wrap around a cylinder, with every entry at most N. Letting N grow gives the conjecture. Our computer compares Z and P coefficient by coefficient for ten pairs, including four and five up to q^22, and they agree. That is an illustration, not a proof.

What it doesn’t claim

What is not claimed. The link between the matrix counts and the q-series is a theorem of Huang, Jiang and Oblomkov that this paper quotes, and the Lean statement is about the q-series and the product, not about matrices. The paper does not say that an AI found the proof on its own; it says the authors set the direction. A positivity result it derives, toward a conjecture of Corteel and Warnaar, covers only these balanced profiles. And the cases with a equal to two or three were known before.

Where it stands

Preprint

arXiv 2609.20567: version 1, September 17, 2026; version 2, October 7, 2026

Independent expert review

None named in our sources (the paper thanks colleagues for discussions)

Peer reviewed

No

Lean proof, by Axiom

Formalized with AxiomProver. The repository’s README says this version was run against the Lean comparator on October 7, 2026, which reported “Your solution is okay!”. Not built or run by us

Last checked October 27, 2026. Where it stands, as of October 27. It is a preprint, at version two. Expert review: none of our sources names an independent reviewer; the paper thanks colleagues for discussions. It has not been peer reviewed. The Lean is by Axiom. Its README says this version was run against the Lean comparator on October 7, which reported: your solution is okay. Its automated GitHub build is also marked as passing. The comparator allows only Lean’s three standard axioms. Our text scan of its 860 Lean files finds sorry only in the challenge file, where it marks the statements, and no new axioms and no native_decide. One caution: the conjecture’s statement is defined in Axiom’s own q-series library, so readers must check that definition too. We did not build or run any of it.

If it holds, every coprime pair a and b gives an identity of Rogers–Ramanujan type, and, through Huang, Jiang and Oblomkov’s theorem, the normalized counts of commuting nilpotent matrices with A^a = B^b add up to an explicit infinite product, with the first Rogers–Ramanujan identity as the simplest case.

How the proof goes

1. Two branches, one equation. How the proof goes, in the paper’s account. Two generating series are shown to satisfy the same q-difference equation, whose coefficients count rational Dyck paths, lattice paths that stay above a diagonal, weighted by their area. A solution that starts with one is unique. The first branch starts from the HJO sums. Expanding their Gaussian factors as words of filters on the gaps turns them into Dyck paths that return to the diagonal at prescribed points. Then the compositional rational shuffle theorem, from work of Bergeron, Garsia, Leven and Xin, and of Mellit, together with a multiplicativity theorem for slope operators, gives the equation. The second branch starts from the cylindric partitions. A bijection matches them with collections of disjoint cycles in a weighted graph, and a finite determinant, expanded by Cramer’s rule, gives the same equation. Uniqueness makes the two series equal. Finally, Huang’s bound on the quadratic form lets N go to infinity, and the known product for unbounded cylindric partitions, from Borodin and from Foda and Welsh, finishes the conjecture. The authors credit Ole Warnaar with the observation that the HJO series could be framed with cylindric partitions. Our brute-force count matches the finite identity, up to a fixed power of q, in eight small cases.
2. The build-up. The build-up, as the repositories record it. In August, the paper for a equal to three came with a Lean repository that assumed eight facts from the literature, including Warnaar’s identities; its latest automated build, on August 26, is marked as failed. The four small cases came with a repository whose HJO statements assumed Warnaar’s theorem. The new paper says the a = 3 method of Lau and Ono does not easily extend to general a. For the full conjecture, the first version of the HJO repository, on September 10, assumed eight results from the literature. Four days later, two remained: a commutation theorem for slope operators, and the shuffle identity. Version one of the paper said the Lean was conditional on those two. On October 7, a commit titled HJO is proved unconditionally was merged. The Lean had grown from about 21,000 lines to about 308,000, by our count.
3. The AI’s role. What did the AI do? The paper says it was written using human-AI collaboration with AxiomProver, through literature search, significant numerical experimentation, and the proposal and rejection of many candidate strategies. At every stage, it says, the authors set the direction and made the mathematical judgments, and they take full responsibility for the correctness of the results. The formalization was done with AxiomProver, against a challenge file that the paper says was written by humans.

The numbers in the video

• Ours: partitions of 6 into parts differing by at least 2 (6, 5+1, 4+2) and into parts congruent to 1 or 4 mod 5 (6, 4+1+1, 1+1+1+1+1+1): three each; the two counts agree for every n up to 40.
• Ours: pairs of commuting nilpotent matrices over the field with two elements with A³ = B⁴: 1, 10 and 400 pairs of size 1, 2 and 3 (brute force).
• Ours: Z(q) = P(q) coefficient by coefficient for ten pairs: (2,3) through q^40, (2,5) through q^20, (2,7) through q^16, (3,4) through q^30, (3,5) through q^20, (3,7) through q^14, (3,8) through q^12, (4,5) through q^22, (4,7) through q^10, (5,6) through q^6. An illustration, not a proof.
• Ours: the finite identity (Theorem 1.1) by brute-force counts of cylindric partitions in 8 small cases; the paper’s (4,5) example F₂(1) = 196 reproduced.
• Ours: Lean lines in the HJO repository: 2026-09-10: 20,971 lines in 46 files, 8 literature results assumed; 2026-09-14: 33,743 lines in 95 files, 2 literature results assumed; 2026-10-07: 308,118 lines in 860 files, 0 literature results assumed. Our text scan of the last version: sorry only in the challenge file, no axiom declarations, no native_decide.

Read the source

• Yifeng Huang, Kenny Lau, Ken Ono, “Rogers–Ramanujan identities from the geometry of X^a = Y^b”, arXiv 2609.20567 (v2, October 7, 2026), 38 pages.
• Kenny Lau, Ken Ono, “Modularity of Point Counts for the Curves X^a = Y^b: New Rogers–Ramanujan Identities”, arXiv 2608.05480 (the a = 3 case).
• Yifeng Huang, Kenny Lau, Ken Ono, Peter Paule, “Algebraic geometric framework of Rogers–Ramanujan identities”, arXiv 2608.15219 (four small cases).
• Lean repositories (not run by us): AxiomMath/HJO, AxiomMath/RR_a3, AxiomMath/HJOa3Small.

AI Proved What? is independent and not affiliated with Axiom Math.

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.