Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs
The geometric extension of the Rogers-Ramanujan and Andrews-Gordon identities conjectured by Huang, Jiang and Oblomkov is proved for every torus-knot singularity with coprime exponents, via a stronger finite identity.
- Lab
- Axiom Math
- Model
- AxiomProver
- Field
- Mathematics
- Date
- 2026-09-17
- Human collaborators
- Yifeng Huang, Kenny Lau, Ken Ono
What was found
The conjecture of Huang, Jiang and Oblomkov gives a geometric extension of the Rogers-Ramanujan and Andrews-Gordon identities for the torus-knot singularity X^a = Y^b with coprime exponents. The paper establishes a threefold equality between a normalized count of pairs of commuting nilpotent matrices over a finite field satisfying A^a = B^b, the HJO q-series, and an explicit infinite product. The main result is stated as a stronger finite identity, that the rank N HJO sum equals a q-Pochhammer factor times the generating function for balanced cylindric partitions with entries bounded by N, with the conjecture following in the limit. The proof is human mathematics: it combines the compositional rational shuffle theorem of Bergeron, Garsia, Leven and Xin and of Mellit with a multiplicativity theorem for slope operators and a determinantal model, linked by a common q-difference equation. The abstract's AI disclosure covers the formalization only: the finite identity and the HJO conjecture have been formalized in Lean by AxiomProver, conditional on two stated literature inputs.
Novelty check
The 2026-09-23 watch run searched arXiv and the web for the a = 3 layer specifically and found two August 2026 papers by an overlapping author set, arXiv:2608.05480 and arXiv:2608.15219, which resolve individual exponent pairs rather than a full family; no prior resolution of the general coprime case was found. That search was not a systematic review of the Rogers-Ramanujan and torus-knot-singularity literature, and whether this paper generalizes rather than restates those two predecessors is the first thing a specialist should check. The year the HJO conjecture was posed is not stated in the abstract and is left unrecorded here rather than guessed.
Caveats and known objections
Autonomy is ai-assisted rather than anything stronger because the abstract places AxiomProver on the formalization, not on the discovery: the proof strategy it names is a combination of existing human theorems. Verification is claimed rather than formal for the reason the abstract itself supplies, that the Lean development is conditional on two stated literature inputs, so what the kernel establishes is an implication rather than the theorem outright, the same structure as this registry's 2026-09-02-prime-gaps-186 entry. Whether those two inputs, the collinear commutation of slope operators and the compositional rational shuffle identity, are settled literature or are doing substantive unproved work is the question that decides how much the formalization is worth. A preprint days old at entry, unrefereed, with no mathematician review found as of 2026-09-22 and no third-party audit of the Lean statements against the paper.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-assisted.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-assisted for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-17-rogers-ramanujan-torus-knotBibTeX
@misc{whataifound-axiommath-2026-knot,
title = {Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Axiom Math. Verification: Claimed. Autonomy: AI-assisted.},
url = {https://whataifound.org/finding/2026-09-17-rogers-ramanujan-torus-knot}
}