Selected Publications | Axiom
Our selected publications
Research and publications from the Axiom team
BEYOND MOCK MODULARITY: ELLIPTIC CORRECTIONS FOR HIGHER DYSON RANKS
Date: July 14, 2026
Axiom 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.
Read article
RECORD COMPOSITIONS OF ALTERNATING PERMUTATIONS
Date: July 13, 2026
Axiom 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.
Read article
INTEGER VALUES OF ARCTANGENT SUMS ARE RARE
Date: July 7, 2026
Axiom 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.
Read article
FORMALIZED q-SERIES: THE ROGERS–RAMANUJAN IDENTITIES AND BEYOND
Date: July 2, 2026
Axiom 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.
Read article
THAKUR’S HYPOTHESES ON POWER SUMS OVER Fq[t]
Date: June 14, 2026
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.
Read article
DOMINANT ZEROS OF NEKRASOV–OKOUNKOV POLYNOMIALS
Date: June 14, 2026
Bernhard 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.
Read article
A PROBLEM OF ANDREWS AND DHAR ON PARTITIONS
Date: June 3, 2026
Motivated by a broad question about the potential of AI-assisted mathematics, this work investigates whether an AI system can help discover and certify an explicit bijection between two infinite sequences of complicated combinatorial sets already known to be equinumerous. The challenge requires finding a reversible structure that explains this equality uniformly across the sequence. Providing an affirmative test case within a partition problem introduced by Andrews and Dhar, a residue-class equidistribution theorem is proved to identify a "canonical third" subset. Through human-AI collaboration, the required bijection is constructed as a highly structured composition of four maps. The equidistribution theorem itself was autonomously produced by Axiom Prover and formally verified in Lean, demonstrating how collaborative workflows can uncover and formalize deep structural symmetries.
Read article
WE CAN’T AGREE TO DISAGREE, FORMALLY
Date: May 26, 2026
Axiom Math Staff and Harvard Business School Professor Scott Duke Kominers use Lean to formalize Nobel laureate Robert Aumann’s classic theorem on why rational agents with shared beliefs cannot have common knowledge that they disagree. The paper treats the theorem as a case study in “assumption accounting”: showing how formal proof can verify a familiar argument while also exposing exactly which economic and mathematical assumptions make the conclusion possible.
Read article
Reciprocals of Partition Polynomials
Date: May 20, 2026
Axiom Staff study reciprocal sums built from partition “subsum polynomials,” addressing ten conjectures posed by Ballantine, Beck, Feigon, and Maurischat. They prove six of the conjectures using elementary number theory and cyclotomic polynomials, while AxiomProver autonomously produced Lean/mathlib formalizations of the proofs and discovered a counterexample to one statement as originally posed.
Read article
CHEBYSHEV QUOTIENTS, DEMAZURE MULTIPLICITIES, AND DYCK-PATH MODELS
Date: April 28, 2026
What if we could visualize abstract algebra? In this paper, Rekha Biswal and Axiom Math staff bridge the gap between complex Lie algebra decompositions and visual combinatorics. By proving that certain algebraic sequences are always positive, they show these abstract structures can be mapped out with simple, geometric models like "Dyck paths". AxiomProver autonomously produced and verified the theorems in Lean/mathlib.
Read article
A quadratic form generalization of rational dinv
Date: April 13, 2026
Yifeng Huang introduces a method to analyze geometric structures called Dyck paths, proving that certain calculations within these models remain stable and finite. This stability is essential for understanding the underlying geometry of complex mathematical curves. AxiomMath assisted Huang by using the Axiom Prover system to autonomously formalize the paper’s primary theorem into a machine-verifiable proof. This partnership demonstrates a reliable process for using AI to certify the logic of human-led research, bridging the gap between mathematical discovery and formal verification.
Read article
ABC implies that Ramanujan’s tau function misses almost all primes
Date: March 31, 2026
This paper centers on the great Srinivasa Ramanujan’s mysterious tau function, asking how often it can take prime values. Assuming the abc conjecture, it shows that such prime values are extraordinarily rare, missing almost all primes, while still suggesting a sparse infinity may remain. AxiomProver autonomously proved the main engine and autoformalized it in Lean.
Read article
On the paucity of lattice triangles
Date: March 24, 2026
This paper sits at the crossroads of geometry and dynamics, studying which rational triangles give rise to especially symmetric billiard surfaces. Building on the Mirzakhani–Wright obstruction, named in part for Fields Medalist Maryam Mirzakhani, it shows that such triangles are extraordinarily rare. AxiomProver autoformalized the main engine in Lean.
Read article
Almost all primes are partially regular
Date: February 3, 2026
This paper sits in the landscape of number theory inspired by Fermat’s Last Theorem. It is in algebraic number theory, focusing on the subtle ways prime numbers shape the arithmetic of cyclotomic fields and Bernoulli numbers. It proves that almost every prime avoids a large initial range of the obstructions that cause classical irregularity, with consequences for class groups, modular forms, and algebraic K-theory. AxiomProver autonomously proved the main theorem and autoformalized it in Lean.
Read article
Fel’s Conjecture on syzygies of numerical semigroups
Date: February 2, 2026
This paper sits in commutative algebra, studying the hidden structure of numerical semigroups through the relations inside their associated rings. It settles a conjecture of Leonid Fel by giving a complete general formula and showing why it works. AxiomProver autonomously proved the result and autoformalized it in Lean.
Read article
Parity of k-differentials in genus zero and one
Date: February 2, 2026
This paper lies in geometry and dynamics, studying how flat structures on spheres and tori split into different families. It turns a previously conditional classification into a complete theorem by proving the missing number-theoretic step. AxiomProver autonomously found the key proof idea and autoformalized the central combinatorial condition in Lean.
Read article
Transformers know more than they can tell -- Learning the Collatz sequence
Date: November 12, 2025
This paper sits at the intersection of machine learning and mathematics, using the Collatz sequence to examine what transformers actually learn when performing difficult arithmetic computations. It shows that, although accuracy varies sharply with the numeral base, all models learn the same underlying structure: classes of inputs determined by powers of 2 and the loop lengths built into the computation. The paper gives a mathematically interpretable account of both success and failure, showing that most errors come from misjudging how long the computation should run rather than from producing arbitrary outputs.
Read article