PublicationAug 2026Algebraic Geometric Framework of Rogers–Ramanujan IdentitiesAxiom Math staff together with Yifeng Huang and Peter Paule have proved the first four non-trivial cases of the Huang–Jiang–Oblomkov conjecture. The classical Rogers–Ramanujan identities equate infinite q-series governed by quadratic forms to infinite products with modular symmetry, but finding the structures that generate such families remains a fundamental challenge. The conjecture proposes a powerful new origin in algebraic geometry: counts of commuting nilpotent matrix pairs on plane curve singularities $x^a$=$y^b$ naturally yield broad families of these identities. Focusing on the a=3 layer, the team proved a finer sum-to-sum identity that settles the conjecture for b=4,5,7, and 8. AxiomProver formalized and verified these algebraic identities in Lean, providing an end-to-end formal certificate for the proofs.arXiv ↗
PublicationAug 2026Parity of the Partition Function in Quadratic ProgressionsAxiom Math staff mathematicians have proved a conjecture from 2010 on the parity of the partition function. Count the ways to break a number into a sum of positive integers and you get p(n); ask only whether that count is even or odd and you hit one of the most stubborn walls in the subject. The conjecture picks out a thin quadratic sliver of the integers — the values (Dm² + 1)/24, for squarefree D congruent to 23 mod 24 — and predicts that even and odd both keep appearing along it forever. For linear progressions this was settled years ago. For anything of degree two or higher, nothing was known at all. The new paper proves the quadratic case, and does it with geometry: the parity question is converted into a question about special points on a curve, and modulo 2 those points stubbornly refuse to collide. What survives is an obstruction that neither an all-even nor an all-odd pattern could live with. AxiomProver formalized and verified the algebraic identities at the heart of the paper in Lean.arXiv ↗
PublicationAug 2026Modularity of point counts for the curves $X^a = Y^b$: new Rogers–Ramanujan identitiesAxiom Math staff mathematicians have proved the first new layer of a conjecture of Yifeng Huang, Ruofan Jiang, and Alexei Oblomkov. Their conjecture begins with a plane curve — one variable raised to a power, set equal to another variable raised to a different power — and counts, over each finite field, the pairs of commuting nilpotent matrices that satisfy it. Bundle those counts together and they form an infinite series, which the conjecture says always folds into an explicit product, essentially a modular function. Sum-equals-product statements of this kind are Rogers–Ramanujan identities, and for a century they have come out of representation theory and symmetric functions; this conjecture says geometry produces them too. When the first exponent is two, the identities are the classical ones of Rogers, Ramanujan, Andrews, and Gordon. Above two, nothing was known. The new paper proves the exponent-three case in full, for every partner exponent at once: a new infinite family of Rogers–Ramanujan identities, and a geometric source for products Warnaar had reached by other means. AxiomProver verified the new identities in Lean, taking the published literature as given.arXiv ↗
PublicationAug 2026A Bijective Proof of a Partition Theorem of Berkovich and UncuAxiom Math staff mathematicians have answered a question Alexander Berkovich and Ali Uncu asked back in 2016. Take a number and break it into distinct decreasing pieces, then tally the odd pieces two ways: by whether each one sits in an odd or an even position, or by whether each one leaves a remainder of 1 or 3 on division by 4. Berkovich and Uncu found that the two tallies give the same number. Pick any pair of target counts you like, and the same number of partitions hits it either way. Their proof is analytic, and is based on generating functions, which confirm that the totals agree without ever saying which partition goes with which. They wanted more. They asked whether someone could pair them off directly. This new paper provides the answer. It builds the pairing in four steps, each a familiar move from the classical theory, and it runs just as easily backwards: hand it a partition of either kind and it hands back the partner. AxiomProver autonomously formalized and verified the proof in Lean.arXiv ↗
PublicationJul 2026On a Conjecture of Han and Xiong for Fractional Gaussian Binomial CoefficientsAxiom Math staff mathematicians have proved the structural core of a recent conjecture of Guo-Niu Han and Huan Xiong on Gaussian binomial coefficients of fractional index. Han and Xiong extended these classical polynomials to fractional upper index, took the integer trace of the resulting series by discarding the fractional powers, and conjectured that the trace is coefficientwise maximal when the index is one-half. They confirmed this in low degree and along two infinite families of parameters. The new paper proves a single support-dominance theorem that subsumes all of their cases: it settles the conjecture on the entire half-line above one-half, for fractions of arbitrary denominator, and collapses the full two-parameter problem over all positive rationals onto one canonical sequence of unit fractions, only finitely many of which are nontrivial in each degree. What remains of the conjecture is now a single sequence rather than a two-parameter family. AxiomProver autonomously produced, formalized, and verified these results in Lean.arXiv ↗
PublicationJul 2026Beyond Mock Modularity: Elliptic Corrections for Higher Dyson RanksAxiom Math staff mathematicians and Professor Claudia Alfes (U. Bielefeld) have provided the complete function theory for a mathematical challenge dating back to Freeman Dyson in 1944. Dyson originally introduced his "rank" statistic to explain the celebrated integer partition congruences discovered by Srinivasa Ramanujan. While the analytic framework for this foundational m=1 case was famously solved in a 2010 Annals of Mathematics paper, the structure governing the higher Dyson systems for all integers m>1 remained a difficult open problem. The new paper successfully establishes the explicit analytic framework for all of these remaining cases. AxiomProver played a key role in the discovery process, helping to formulate, formalize, and strictly verify the complex algebraic steps in Lean.arXiv ↗
PublicationJul 2026Record Compositions of Alternating PermutationsAxiom Math staff mathematicians have solved an open problem posed by MIT Professor Richard Stanley—widely regarded as the greatest combinatorialist of the last century—and his collaborators. The problem asks for a finer way to count alternating permutations, whose entries repeatedly rise and fall, according to the ordered pattern formed by their successive records. The paper gives an explicit formula for these refined counts and explains their natural connection to noncommutative symmetric functions. It also extends the underlying mechanism to a broad family of combinatorial structures arising from exponential generating functions. The results show how information lost when parts are treated as an unordered partition can be recovered by passing to ordered compositions and a noncommutative setting. The main results were autonomously produced and formally verified in Lean by AxiomProver from natural-language statements of the theorems, providing another demonstration of its ability to carry out research-level mathematics. The paper also marks a special milestone for Axiom Math: it is the first research paper of one of our staff mathematicians.arXiv ↗
PublicationJul 2026Integer Values of Arctangent Sums Are RareAxiom Math staff mathematicians have studied a 2008 conjecture of Amdeberhan, Medina, and Moll concerning the sequence obtained by taking the tangent of the running sum arctan 1 + arctan 2 + ⋯ + arctan n. The first four values are integers, but the conjecture predicts that no integer values occur thereafter. The paper proves that any later integer value, if one exists, must be extraordinarily large, and uses this to show that the conjecture is true for almost every value of n. The argument combines classical ideas from number theory, including Gaussian integers, factorization, divisibility, and estimates for prime numbers, to turn the problem into a sharp arithmetic obstruction. This improves the previously known result from about 15% of cases to all but a logarithmically sparse exceptional set. Most significantly, the main results were 100% autonomously produced and verified in Lean by AxiomProver from natural-language statements of the results, demonstrating AxiomProver’s ability to carry out research-level mathematics in number theory.arXiv ↗
PublicationJul 2026Formalized Q-Series: the Rogers–Ramanujan Identities and BeyondAxiom Math mathematicians formalized significant foundational material in the theory of q-series, a central language connecting partition theory, modular forms, representation theory, and mathematical physics. Formalization means translating mathematical definitions, theorems, and proofs into a proof assistant so that every logical step is checked by machine; this matters because it turns difficult mathematics into reusable, verifiable infrastructure for future research. The paper develops the foundations needed to work rigorously with q-series in Lean and applies them to two landmark results: the Jacobi Triple Product formula and the Rogers–Ramanujan identities. These theorems are both historical benchmarks for the subject and demanding tests for formal proof systems. AxiomProver handled the development and verification of the Lean formal artifact, demonstrating its ability to carry out research-level formal mathematics in a deep classical area.arXiv ↗
PublicationJun 2026Four-digit Kaprekar dynamics in odd basesAxiom Math staff mathematicians, together with Richard E Schwartz and Dinesh Thakur, have analyzed the famous Kaprekar routine for four digits in all odd bases. The Kaprekar routine was a popular piece of recreational mathematics, in which one could start with a four decimal digits (not all the same), arrange the digits in descending and ascending order, take the difference, and then repeat. In base 10, this always ends at the magic number 6174. Previously, much less was known about the behavior for other bases. This new paper resolves the case of odd bases completely for four digits. It shows that a cycle is entered in at most four steps and computes the shape of all terminal cycles that could arise. The main technique of the paper is a careful labeling under which the Kaprekar operation can be recast as a projective doubling.Journal of Integer Sequences, Vol. 29 (2026), Art. 26.4.7arXiv ↗
PublicationJun 2026Dominant Zeros of Nekrasov–Okounkov PolynomialsBernhard Heim and Markus Neuhauser study Nekrasov–Okounkov polynomials that arise from the hook-length formula of Fields Medalist Andrei Okounkov and Nikita Nekrasov. Extending the classical Frame–Robinson–Thrall hook formulas, these polynomials link representation theory with modular forms. The paper proves that each Nekrasov–Okounkov polynomial has a unique zero of maximal modulus by translating the problem into Perron–Frobenius theory for an explicit Hessenberg matrix. It also presents Challenge 3, asking for a conceptual proof of a key positivity theorem. K. Ono’s appendix provides this proof, which was generated and verified autonomously by AxiomProver in Lean.Accepted for publication in Research in Number TheoryarXiv ↗
PublicationJun 2026Thakur’s hypotheses on power sums over $F_q[t]$Motivated by central problems regarding zeta and multi-zeta functions, in 2009, Dinesh Thakur posed three conjectural hypotheses concerning the degrees of finite field function field power sums. Here we prove Hypotheses H1 and H2 for prime fields, giving a unique greedy description of the extremal term in Carlitz’s formula and establishing the recursion predicted by Thakur. We also prove Hypothesis H3 outright over all finite fields, establishing a monotonicity theorem for these power sums. As consequences, these results recover the strict Newton-polygon convexity used in the Carlitz–Goss Riemann hypothesis over prime fields and Thakur’s nonvanishing theorem for positive function-field multizeta values. AxiomProver generated and verified these results in Lean.arXiv ↗