arXiv subjects

Ken Ono

Publications and source records attributed to Ken Ono.

At least 19 recordsLinked to original sources

arXiv2026

Proof of the Lyons--White Conjecture

Let $D_n$ be the dihedral group of order $2n$. Consider a continuous-time random walk on $D_n$ driven by arbitrary symmetric rates whose support generates $D_n$. For $p\in[1,\infty]$, we say the pair $(D_n,p)$ is rate-monotonic if for each fixed time $t$, the $\ell^p$-distance between the random walk's distribution at time $t$ and the uniform distribution is monotonically decreasing as a function of the rates. Lyons and White proved that $(D_n,2)$ and $(D_n,\infty)$ are rate-monotonic. Somewhat counterintuitively, they found several pairs $(D_n,p)$ with ${p\in[1,1.997]\cup[2.001,3.999]\cup[4.001,5.995]}$ that are not rate-monotonic, and they asked whether any such pairs exist with $p=4$ or $p=6$. We resolve their question, proving that $(D_n,2m)$ is rate-monotonic for all positive integers $m$ and $n$. In fact, we prove a generalization of this result to a broader family of groups that includes generalized dihedral groups, dicyclic groups, and generalized quaternion groups. In the other direction, we prove that for every real $p\geq 1$ that is not an even integer, there exists a positive integer $n$ such that $(D_n,p)$ is not rate-monotonic. The results of this paper were formally verified in Lean by AxiomProver assuming standard literature.

math.PR↗

arXiv2026

Zero-free columns in character tables of symmetric groups

The rows and columns of the character table of the symmetric group $S_n$ are both naturally indexed by partitions of $n$. Let $D(n)$ denote the number of conjugacy classes of $S_n$ whose column contains no zero entry. The identity column is always zero-free, so $D(n)\geq 1$. It is known that $D(n)\ll n^2$. We prove that $D(n)\ll n^{3/4}$. Second, we prove for almost all positive integers $n$ that $D(n)\ll_B n^{1/2}(\log n)^B$ for every $B>5/6$, with a quantitative bound for the exceptional set, using work of Matom\"aki and Radziwill. Finally, we offer a heuristic supporting our conjecture that $D(n)\ll_{\varepsilon} n^{\varepsilon}$. AxiomProver formalized the results in this paper in Lean assuming preexisting literature.

math.CO↗

arXiv2026

Algebraic geometric framework of Rogers--Ramanujan identities

The Rogers--Ramanujan identities equate a $q$-series whose exponents are governed by a quadratic form with an infinite product supported on two residue classes modulo~$5$. Identities of this shape are scarce, and a central problem is to identify the structures that produce them in families. Huang, Jiang, and Oblomkov have proposed a source of a new kind: to each pair of coprime integers $a,b>1$ they attach an infinite-rank $q$-series $Z_{a,b}(q)$, assembled from counts of commuting nilpotent matrix pairs $(A,B)$ with $A^a=B^b$ over finite fields, and they conjecture that it equals an explicit product of $(a-1)(b-1)/2$ modular units of level $a+b$. The $a=2$ cases are the Andrews--Gordon identities; no case with $a>2$ was known. We prove the conjecture for $(a,b)=(3,4)$, $(3,5)$, $(3,7)$, and $(3,8)$. Our proofs pass through a finer sum-to-sum identity, which we conjecture for all $b$ coprime to $3$ and establish for all $b$ when $q=1$. Lau and Ono have since proved that identity in general, and with it the full $a=3$ case. These identities have been formalized and verified in Lean by AxiomProver.

math.NT↗

arXiv2026

Modularity of Point Counts for the Curves $X^a=Y^b$: New Rogers--Ramanujan Identities

For coprime $1<a<b$, let $M_n^{a,b}(\mathbb{F}_q)$ be the set of commuting pairs of nilpotent $n\times n$ matrices over $\mathbb{F}_q$ with $X^a=Y^b$. Huang, Jiang, and Oblomkov assembled their orders as an Eulerian $q$-series $Z_{a,b}(q)$. They conjectured that it is an explicit product $P_{a,b}(q)$ involving Jacobi's theta function and Dedekind's eta-function, implying the threefold equality $$\underbrace{\prod_{n\ge1}(1-q^n)\cdot\Biggl(\sum_{n=0}^{\infty}\frac{|M_n^{a,b}(\mathbb{F}_q)|}{|\mathrm{GL}_n(\mathbb{F}_q)|}\Biggr)\Biggr|_{q\mapsto q^{-1}}}_{\text{point count}}\;=\;\underbrace{Z_{a,b}(q)}_{q\text{-series}}\;=\;\underbrace{P_{a,b}(q)}_{\text{theta quotient}}$$ If true, the point count on $X^a=Y^b$ is essentially a modular function on $\Gamma(a+b)$. The conjecture is layered in $a$, with an identity for each $b$. The $a=2$ layer is classical, including identities of Rogers--Ramanujan and Andrews--Gordon. For $a\geq3,$ nothing was known. We prove the $a=3$ layer in full: a new infinite family of Rogers--Ramanujan identities, and a geometric origin for Warnaar's products. AxiomProver verified these new identities in Lean assuming existing literature.

math.NT↗

arXiv2026

A bijective proof of a partition theorem of Berkovich and Uncu

In 2016, Berkovich and Uncu proved that, for all nonnegative integers $i$, $j$, and $n$, the number of strict partitions of $n$ with $i$ odd-indexed odd parts and $j$ even-indexed odd parts equals the number of strict partitions of $n$ with $i$ parts congruent to $1$ modulo $4$ and $j$ parts congruent to $3$ modulo $4$. Their proof used generating functions, and they asked for a combinatorial proof. We answer their question with an explicit bijection, assembled from three classical ingredients: $2$-modular diagrams, an insertion algorithm of Chen, Gao, Ji, and Li, and Glaisher's bijection. AxiomProver autonomously formalized and verified the proof of the main theorem in Lean.

math.CO↗

arXiv2026

On a conjecture of Han and Xiong for fractional Gaussian binomial coefficients

Han and Xiong recently extended the Gaussian binomial coefficient $\genfrac{[}{]}{0pt}{}{r+k}{k}_{q}$ to positive rational $r$ and conjectured that its integer trace, the integer-exponent part of the resulting power series, is coefficientwise largest at $r=1/2$. We prove a support-dominance theorem comparing rational parameters under an explicit divisibility condition. It settles the conjecture for every $r\geq 1/2$ and reduces the full conjecture to the unit fractions $r=\frac{1}{2m}$, only finitely many of which are nontrivial for each fixed $k$. A computer computation then verifies the conjecture for every positive rational $r$ and every $k\leq 200$. The theoretical results were autonomously produced and verified in Lean by AxiomProver.

math.CO↗

arXiv2026

Record compositions of alternating permutations and noncommutative symmetric functions

Amdeberhan, Shareshian, and Stanley recently proved that a function $\varphi$ arising in the theory of partition Eisenstein series counts the alternating permutations of $\{1,\dots,2n\}$ with a given `record' partition, and they asked whether there is a similar theory for record compositions, suggesting a role for noncommutative symmetric functions. Here we solve their open problem by showing that the number of alternating permutations of $\{1,\dots,2n\}$ with record composition $(\alpha_1,\dots,\alpha_\ell)$ is \[ \prod_{j=1}^{\ell}\binom{2s_j-1}{2\alpha_j-1}E_{2\alpha_j-1}, \] where $s_j=\alpha_1+\dots+\alpha_j$, $E_k$ is an Euler number, and the record composition of $w=a_1a_2\dots a_{2n}$ (so $a_1>a_2 \dotsb$) lists the factor lengths obtained by cutting $a_1a_3\dots a_{2n-1}$ before each left-to-right maximum other than the first. These numbers are the coefficients of a natural lift of the degree-$n$ sprout symmetric function with seed $\sec(\sqrt{t}\,)$ to noncommutative symmetric functions, expanded in products of noncommutative power sums of the first kind. An analogous refinement holds for every sprout sequence whose seed is given by the exponential formula. AxiomProver autonomously produced and verified the results in this paper in Lean.

math.CO↗

arXiv2026

Beyond Mock Modularity: Elliptic Corrections for Higher Dyson Ranks

When $m = 1$, the Dyson rank generating function is a classical bridge between partition theory, Ramanujan's mock theta functions, and the theory of harmonic Maass forms and nonholomorphic Jacobi forms. The rank is a statistic on partitions, and the higher Dyson systems, for $m \geq 2$, are a natural multivariable refinement of it, combining $m$ graded rank contributions. Unlike the classical case, these higher systems are not expected to fit the mock-modular framework, which raises the question of what analytic structure governs them. We show that their root-of-unity specializations carry a hidden elliptic structure. A finite $q$-difference recurrence produces an explicit polynomial obstruction to the expected index $m$ elliptic transformation law, and because the obstruction is finite, its partial fractions canonically determine finitely many Appell--Lerch correction terms that remove it. The corrected functions satisfy a twisted index $m$ elliptic law; a natural translation removes the twist, and their holomorphic finite parts admit finite theta decompositions. Thus, the natural analogue of Dyson's mock-modular phenomenon at higher $m$ is not mock modularity but a finite theta decomposition governed by an index $m$ elliptic transformation law. These results grew out of a human--AI collaboration, and the key new formulas were formalized and machine-verified in Lean/Mathlib by AxiomProver.

math.NT↗

arXiv2026

Integer values of $\tan(\arctan 1+\arctan 2+\cdots+\arctan n)$ are rare

For $n\ge1$, we let $$x_n:=\tan\bigl(\sum_{k=1}^{n}\arctan k\bigr).$$ In 2008, Amdeberhan, Medina, and Moll conjectured that $x_n\not \in \mathbb{Z}$ for every $n\ge5$. This was known for a set of positive integers of density $\tfrac{120}{817}\approx0.1469$. We prove that an integer value $x_n=m$ satisfies $|m|\ge e^{(1/2+o(1))\,n\log n}$, which we use to deduce that $$\#\{\,1\leq n\le N:x_n\in\mathbb{Z}\,\}=O(\log N). $$ In particular, the conjecture holds for a density-one set of $n$. The results in this note were formalized in Lean/Mathlib and produced autonomously by AxiomProver from natural-language statements.

math.NT↗

arXiv2026

Formalized $q$-series: The Rogers-Ramanujan Identities and Beyond

The theory of $q$-series and basic hypergeometric series plays a crucial role at the intersection of combinatorics, number theory, and representation theory. From the classical partition identities of Euler and Jacobi to modern developments in class field theory, vertex operator algebras, and the Monstrous Moonshine conjecture, $q$-series provide the analytic framework for a wide range of profound applications. In this paper, we discuss the formalization of this theory in the Lean proof assistant, a process that requires careful design of scalable and versatile structures to reconcile formal algebraic identities with analytic convergence properties. We address these foundational challenges by focusing on the construction of $q$-Pochhammer symbols, $q$-binomial coefficients, Bailey's Lemma and similar primitives. To demonstrate the utility of this work, we provide fully verified proofs of the Jacobi Triple Product formula and the celebrated Rogers-Ramanujan identities, which serve as both historical and technical benchmarks for the field. This work establishes a rigorous computational foundation for the future formalization of mock theta functions, modular forms, and the diverse algebraic structures that underpin their applications across mathematics and physics. AxiomProver was used to produce the formalizations in this paper.

math.NT↗

arXiv2026

Four-digit Kaprekar dynamics in odd bases

Start with four digits, arrange them in both descending and ascending order, subtract, and repeat. This simple process is known as the Kaprekar routine, famous in base ten for sending every nonconstant four-digit string to $6174$. We show that in every odd base $B>3$, the four-digit Kaprekar map has an unexpectedly rigid structure. After at most three iterations, every nonconstant orbit enters an explicit triangular region $\mathcal{T}_B$, and on this region the map is conjugate to projective doubling: \[ \{[r],[s]\}\longmapsto \{[2r],[2s]\}. \] This gives a complete finite description of all nonconstant terminal cycles, including an explicit formula for their lengths and counts. In particular, the longest terminal cycle has length at most $(B-1)/2$, and equality can occur only when $B$ is prime. For primes $p>5$, equality occurs precisely when the least positive $m$ with $2^m\equiv\pm1\pmod p$ is $m=(p-1)/2$. The results proved here were first formulated by Schwartz and Thakur. As a test case for AI-assisted formal mathematics, AxiomProver produced Lean/mathlib formalizations of these results.

math.NT↗

arXiv2026

Thakur's hypotheses on power sums of $\mathbb{F}_q[t]$

In his 2009 paper, Thakur posed three conjectural hypotheses for the degrees of the power sums \[ S_d(k)=\sum_{\substack{a\in \mathbb F_q[t] \text{ monic}\\ \deg a=d}} a^{-k} \qquad\text{and}\qquad s_d(k)=-\deg_t S_d(k). \] For prime fields $q=p$, we prove Hypotheses H1 and H2, giving a unique greedy description of the extremal term in Carlitz's formula and establishing the recursion \[ s_d(k)=s_{d-1}(s_1(k))+s_1(k). \] As consequences, the prime-field recursion gives the strict Newton-polygon convexity used in the prime-field Carlitz-Goss Riemann-hypothesis theorem, and it recovers Thakur's nonvanishing theorem for positive multizeta values over $\mathbb F_p[t]$. We also prove Hypothesis H3 for all finite fields $q=p^f$, establishing the monotonicity \[ s_d(k)<s_d(k+1)\qquad (p\nmid k). \] We provide Lean formalizations of the arguments in this paper, generated by AxiomProver.

math.NT↗

arXiv2026

A problem of Andrews and Dhar on partitions

This paper is motivated by a broad question about AI-assisted mathematics: can an AI system help discover and certify an explicit bijection between two infinite sequences of complicated combinatorial sets already known to be equinumerous? The challenge is to find a reversible structure explaining that equality uniformly across the sequence. We give an affirmative test case in the setting of a partition problem. Andrews and Dhar introduced two partition families $\mathcal{C}_3(n)$ and $\mathcal{D}_3(n)$, and for "nonexceptional'' $n$, they asked for a bijective proof of their equality \[ |\mathcal{C}_3(n)|=\frac{|\mathcal{D}_3(n)|}{3}. \] We prove a residue-class equidistribution theorehm for $\mathcal{D}_3(n)$ that identifies a "canonical third'' subset $\mathcal{D}_3^{(0)}(n)\subseteq \mathcal{D}_3(n)$. Answering their question, we construct a bijection \[ \iota_n:\mathcal{C}_3(n)\longrightarrow \mathcal{D}_3^{(0)}(n) \] as a highly structured composition of four maps. AxiomProver autonomously produced and Lean-verified the equidistribution theorem. The bijection was found through human--AxiomProver collaboration, and the theorem was autoformalized and verified by the system.

math.CO↗

arXiv2026

Reciprocals of Partition Polynomials

Ballantine--Beck--Feigon--Maurischat introduced the subsum polynomial \[ \operatorname{sp}(\lambda,x):=\prod_i (1+x^{\lambda_i}) \] attached to an integer partition $\lambda$, and studied rational functions obtained by summing reciprocals of these polynomials over natural classes of partitions. They posed ten conjectures which naturally divide into coprimality and divisibility questions, special-value and recurrence formulas, and coefficient-shape problems. We prove all of the conjectures in the first two families: the ordinary and binary coprimality/divisibility conjectures, and the odd and ternary special-value/recurrence conjectures. AxiomProver autonomously produced Lean/mathlib formalizations and machine-checkable proofs of these six conjectures, and also discovered a counterexample to the statement as printed; the corrected form remains open.

math.CO↗

arXiv2026

Chebyshev quotients, Demazure multiplicities, and Dyck-path models

We study Chebyshev quotients that arise in the representation theory of Lie algebras, specifically within the theory of Demazure flags for fusion products of $\mathfrak{sl}_2[t]$-modules. Using a recent formula that expresses numerical Demazure multiplicities as coefficients of such quotients, we prove a general eventual non-negativity theorem for the same rational functions that compute these multiplicities: each quotient either terminates or has strictly positive coefficients for sufficiently large degrees, which we in turn interpret in terms of matchings and bounded walks. In several natural infinite families, these are unsigned bounded Dyck path models, giving both a structural explanation for the observed positivity phenomenon and concrete combinatorial models for key families of Demazure multiplicities. The theorems in this paper were autonomously produced and formalized in Lean/Mathlib by AxiomProver from natural-language statements.

math.RT↗

arXiv2026

ABC implies that Ramanujan's tau function misses almost all primes

Lehmer conjectured that Ramanujan's tau-function never vanishes. In a related direction, a folklore conjecture asserts that infinitely many primes arise as absolute values of Ramanujan's tau-function. Recently, Xiong showed that these prime values form a subset of the primes with density at most $2/11$. Assuming the $abc$ Conjecture, we prove the stronger upper bound \[ S(X):=\#\{\ell\le X:\ \ell\ \text{prime and } |\tau(n)|=\ell \text{ for some } n\ge 1\} = O(X^{13/22}), \] which implies that Ramanujan's tau-function misses a density 1 subset of the primes. We give a heuristic suggesting that $S(X)$ should nevertheless be infinite, with predicted order of magnitude \[ S(X)\asymp \frac{C X^{\frac{1}{11}}}{(\log X)^2}. \] The main engine in this note was formalized and produced automatically in Lean/Mathlib by AxiomProver from a natural-language statement of the problem.

math.NT↗

arXiv2026

On the paucity of lattice triangles

A rational triangle $T$ (one whose angles are rational multiples of $\pi$) unfolds to a translation surface ${X_T}$. The lattice triangle problem asks to classify those $T$ for which ${X_T}$ is a Veech (lattice) surface, which means that the $\operatorname{SL}_2(\mathbb R)$-orbit of ${X_T}$ is closed in its stratum (so its projection to moduli space is a Teichm\"uller curve). The most mysterious regime is the "hard obtuse window" (largest angle in $(\pi/2,2\pi/3]$), where it is conjectured that no lattice triangles exist. Using an arithmetic reformulation of the Mirzakhani-Wright rank obstruction, we prove a quantitative theorem that rules out all but a proportion $n^{-1+o(1)}$ of the triangles in this window with denominator $n$. The main technical result in our proof was autoformalized by AxiomProver in Lean (using mathlib).

math.DS↗

arXiv2026

Almost all primes are partially regular

For odd primes $p$, we let $K_p:=\mathbb{Q}(\zeta_p)$ be the $p$th cyclotomic field and let $\omega$ denote its Teichmuller character. For $\alpha>1/2$, we say that an odd prime $p$ is partially regular if the eigenspaces of the $p$-Sylow subgroup of $\operatorname{Cl}(K_p)$ under the Galois action vanish for all characters $\omega^{p-2k}$ with \[ 2\le 2k \le \frac{\sqrt{p}}{(\log p)^{\alpha}}. \] Equivalently, $p\nmid \operatorname{num}(B_{2k})$ throughout this range. We prove that a density-one subset of primes is partially regular in this sense. By Leopoldt reflection, this yields a partial Vandiver Theorem: for a density-one set of primes $p$, the even eigenspaces $A_p(\omega^{2k})$ vanish for all even $2k$ satisfying the inequality above. This result has consequences for Kubota-Leopoldt $p$-adic $L$-functions, congruences between cusp forms and Eisenstein series, and $p$-torsion in algebraic $K$-groups. The theorem proving partial regularity for almost all $p$ is fully formalized in Lean/Mathlib and was produced automatically by AxiomProver from a natural-language statement of the conjecture.

math.NT↗