PublicationOct 2026Explicit Positive Lower Density for the Collatz ConjectureAxiom Math’s Kenny Lau has sharpened a recent theorem on the Collatz conjecture, one of mathematics’ most notorious open problems. Pick a positive integer. If it is even, halve it. If it is odd, triple it and add 1. Repeat. Will you always reach 1? The rules fit on a napkin, but proving that every starting value reaches 1 is another matter! Lech Mazur proved that a positive proportion of starting values reach 1 quickly. Kenny’s paper improves the quantitative bounds, giving an explicit lower bound for that proportion and an explicit threshold beyond which it applies. The guaranteed fraction is tiny, but it does not shrink as the range of starting values grows. 2610.00249v1 Asked to formalize and improve Mazur’s work, AxiomProver autonomously developed the refinement and formalized the main result in Lean. 2610.00249v1arXiv ↗
PublicationOct 2026Ternary Polynomial Relations and Periods of Cusp FormsAxiom Math mathematicians have proved a conjecture of Bachmann and van Ittersum about polynomials in three variables satisfying two special algebraic rules involving symmetry and rearrangement of variables. The conjecture predicted that every such polynomial must be built from simpler polynomials involving only two variables at a time. This work proves the conjecture and goes further, completely classifying all solutions through modular forms, highly symmetric functions central to number theory. The result reveals a surprising connection between elementary-looking polynomial equations and deep mathematical structures. Developed through weeks of human–AI collaboration, the main theorems and essential argument were formally verified in Lean with AxiomProver.arXiv ↗
PublicationOct 2026A Quasi-Riemann Hypothesis for Dedekind Zeta FunctionsAxiom Math mathematicians have proved a quasi-Riemann hypothesis for every Dedekind zeta function. The Riemann hypothesis is one of the deepest open problems in mathematics. It predicts that the zeros of the Riemann zeta function all line up perfectly, which would mean the prime numbers are spread out as evenly as possible. Mathematicians conjecture the same thing for Dedekind zeta functions, one for every number field, extending the classical case to a vast universe of number systems. The full conjecture remains out of reach, but a “quasi” version keeps the zeros out of a band of width 1/32 along the edge. Building on recent work on Artin’s famous Primitive Root Conjecture, the team proved this for every number field at once, and AxiomProver formalized and verified the proof in Lean. The result went to work immediately. The very next day, Fields medalist Manjul Bhargava used it to show that every whole number other than −1 and the perfect squares is a primitive root, meaning its powers cycle through every nonzero remainder, for a positive proportion of primes, a major step toward Artin’s conjecture.arXiv ↗
PublicationOct 2026Local Factors in the BSD Conjecture: A Unified Statistical ViewAxiom Math staff and collaborators David Angdinata and Sameera Vemulapalli have established a unified statistical framework for Tamagawa numbers, important local factors in the Birch–Swinnerton-Dyer conjecture. Using a multivariable Euler product derived from Tate’s algorithm, the team proves new limiting distributions, exact covariance formulas, and moment and tail bounds for Tamagawa products of elliptic curves. Among the results, approximately 50.5% of elliptic curves have trivial Tamagawa product, 42.2% have exactly one prime contributing a nontrivial local factor, and 6.8% have exactly two. The paper also establishes negative correlations between distinct prime-adic valuations of Tamagawa products. AxiomProver autoformalized the results in Lean.arXiv ↗
PublicationSep 2026Cutoff for the Adjacent Transposition Shuffle on a CycleAxiom Math mathematicians have proved that the adjacent transposition shuffle on a cycle exhibits the cutoff phenomenon. Imagine starting with a sorted deck of $n$ cards. At each step, choose two adjacent cards uniformly at random and swap them. Lacoin proved that this shuffling procedure, called the adjacent transposition shuffle, exhibits the cutoff phenomenon. This means the deck of card stays fairly "unmixed" for a long time before suddenly becoming fairly "mixed" withing a short window of time. The adjacent transposition shuffle on a cycle is a mild variant of this shuffling procedure in which one considers the top and bottom cards of the deck to be adjacent so that they also occasionally swap. Proving cutoff for this variant has resisted efforts until now, mostly because the key ingredients needed for Lacoin's proof break down. AxiomProver formalized and verified this result in Lean, assuming existing literature.arXiv ↗
PublicationSep 2026Rogers–Ramanujan identities from the geometry of $X^a=Y^b$Axiom Math mathematicians have proved the HJO conjecture, giving a geometric extension of the classical Rogers–Ramanujan and Andrews–Gordon identities for every torus-knot singularity $X^a=Y^b$ with coprime $1<a<b$. The result connects three seemingly different objects: normalized counts of pairs of commuting nilpotent matrices over finite fields satisfying $A^a=B^b$, the HJO q-series, and an explicit infinite product. The team proves a stronger finite identity, identifying the rank N HJO sum with a generating function for balanced cylindric partitions whose entries are bounded by N; taking N to infinity yields the full conjecture. The proof brings together rational shuffle theory, symmetric functions, cylindric partitions, and a common q-difference equation. AxiomProver formalized and verified the finite identity and the HJO conjecture in Lean, conditional on two stated literature inputs.arXiv ↗
PublicationSep 2026On a Conjecture of Browning and Sawin on Random Hypersurfaces with Sign CoefficientsAxiom Math mathematicians have proved the Browning–Sawin conjecture and obtained a quantitative bound. A general homogeneous polynomial over the complex numbers defines a smooth hypersurface, but this genericity says nothing once every coefficient is restricted to a sign ±1, since the sign vectors form a vanishingly small subset of coefficient space. Browning and Sawin conjectured that smoothness nevertheless holds with probability tending to one as the degree grows. The team proved this, showing that a degree d form in n+1 variables with independent uniform coefficients in {−1,1} defines a singular complex hypersurface with probability Oₙ(d^(−1/2)), and that positive-dimensional singular loci occur with exponentially small probability. AxiomProver formalized and verified these results in Lean, assuming existing literature.arXiv ↗
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 ↗