Number Theory [math.NT]

Elementary anabelian varieties are anabelian
math.NT
math.AG


Magnus Carlson

We show that isomorphisms of fundamental groups of elementary anabelian varieties -- varieties obtained as iterated fibrations of hyperbolic curves -- over sub-$p$-adic fields correspond bijectively to isomorphisms of varieties. Moreover, dominant maps between proper elementary anabelian varieties are in bijection with ``stably cohomologically injective'' maps of fundamental groups: open maps whose pullbacks to all open subgroups induce injections on cohomology rings with $\ell$-adic coefficients, for any prime $\ell$. This verifies conjectures of Grothendieck from his letter to Faltings. Finally, we establish \'etale homotopical generalizations of these results.

Linear recurrences and rational Lambert series
math.NT


Igor Rivin

For a sequence $\gamma=(\gamma_n)_{n\ge 1}$, define \[ L_\gamma(z):=\sum_{n\ge 1}\gamma_n\frac{z^n}{1-z^n} =\sum_{n\ge 1}\Bigl(\sum_{d\mid n}\gamma_d\Bigr)z^n. \] We prove a short rigidity theorem: if $\gamma$ is eventually linearly recurrent and $L_\gamma(z)$ is rational, then $\gamma$ is finitely supported. Equivalently, among sequences with rational ordinary generating function, the only ones whose Lambert series is rational are the finitely supported sequences. The proof specializes the data at a finite place of a finitely generated ring and then uses the periodicity of recurrences over finite fields.

Trilinear Kloosterman fractions I: partially fixed moduli and unbalanced convolutions
math.NT


Thomas Wright

In this paper, we improve on Fouvry and Radziwi{\l}{\l}'s results on unbalanced convolutions. In particular, we find that if $(\alpha_m)$ and $(\beta_n)$ are sequences supported on $m\sim M$ and $n\sim M$ where $\beta$ is equidistributed for small moduli, then \begin{gather*}\sum_{q\sim Q}\left|\mathop{\sum\sum}_{\substack{n\sim N,m\sim M \\ mn\equiv a\pmod q}}\alpha_m\beta_n-\frac{1}{\phi(q)}\mathop{\sum\sum}_{\substack{n\sim N,m\sim M \\ (mn,q)=1}}\alpha_m\beta_n\right|\ll \frac{X}{\log^A X}, \end{gather*} as long as $\exp((\log x)^{\varepsilon}) \leq N \leq Q^{-11/12} X^{17/36-\varepsilon}$ with $Q\leq X^{1/2+1/66-\delta}$, along with wider bounds for $N$ if $Q\leq X^{\frac{45}{89}-\epsilon}$. The former improves the allowable range of $N$, while the latter improves the range of $Q$. To prove these new bounds, we improve Bettin and Chandee's famous result on trilinear forms with Kloosterman fractions in the case where the denominator has a fixed factor.

Reciprocity and the Maslov Phase
math.NT
math.RT


Jonathan Holland

We give a metaplectic proof of Hilbert reciprocity, and hence of quadratic reciprocity, in which the local phase is the Kashiwara--Maslov phase of a triple of Lagrangians. In rank two the phase of the ordered triple $(L_\infty,L_a,L_0)$ is the one-dimensional Weil index $\gamma_v(a)$. The local Hilbert symbol appears as the defect of strict multiplicativity of these phases: \[ (a,b)_v = \frac{\gamma_v(a)\gamma_v(b)}{\gamma_v(1)\gamma_v(ab)}. \] The global step compares the local and adelic realizations of a single Bruhat word for the diagonal torus elements $m(a)\in \operatorname{SL}_2(\mathbb Q)$. Locally the raw Bruhat-word lift carries the normalization factor determined by the chosen quadratic convention. These operators form a projective representation of the diagonal torus with defect \[ \mu_v(a,b) = \frac{\gamma_v(a)\gamma_v(b)}{\gamma_v(1)\gamma_v(ab)}. \] For rational adelic data, the normalized Bruhat word is multiplicative. The reciprocity law states that the total defect $\prod_v\mu_v(a,b)$ is $1$. Combined with the local bridge above, this yields Hilbert reciprocity, while quadratic reciprocity is then the specialization to the pair of odd primes $(p,q)$.

Congruences via Partitions with Exactly Two Part Sizes
math.NT
math.CO


Sittinon Jirattikansakul, Teeradej Kittipassorn, Kraiwich Kongsiri, Nitipon Moonwichit, Kirati Sriamorn

We prove the congruence $\sum_{1 \leq k < \sqrt{N}} \sigma_0 (N - k^2) \equiv 0 \pmod 4$, where $\sigma_0(m)$ denotes the number of positive divisors of $m$, for $N = An + B$ with $(A,B) \in \{ (16,14),$ $(36,30),$ $(72,42),$ $(196,70),$ $(252,114) \}$. Our proof relies on a result of Keith which states that $\nu_2 (N) \equiv 0 \pmod 4$, where $\nu_2(N)$ is the number of partitions of $N$ with exactly two part sizes. Inspired by Dewitt and Keith, our approach combines combinatorial arguments with modular arithmetic techniques.

Additive index and Carlitz rank
math.NT
math.AC


Pierre-Yves Bienvenu, Arne Winterhof

We compare several complexity measures for self-mappings of finite fields. In particular, we show that Carlitz rank and additive index cannot be small simultaneously up to trivial exceptions. That is, these two measures detect cryptographic weaknesses of different classes of functions. We also study the relationship between additive index and degree or weight, respectively, complementing earlier results of Aksoy et al. and G\'omez-P\'erez et al. on the relationship between Carlitz rank and degree or weight, respectively. Finally, we show that a function closely related to the discrete logarithm provides an example in which all four complexity measures, degree, weight, additive index and Carlitz rank, are large.

The Divisor Function along a Deterministic Orbit and the Emergence of Ladders
math.NT
math.CO
math.DS


Marco Mantovanelli

We study the deterministic recursion $n_{j+1} = n_j - \tau(n_j)$, where $\tau(n)$ denotes the divisor function, and the associated orbit length $a(x)$. Heuristics based on the average order of $\tau(n)$ suggest that $a(x) \asymp x / \log x$, but the strong dependence along the orbit places the problem outside the scope of existing methods for multiplicative functions. We develop a deterministic framework that reduces the analysis of the orbit to the distribution of $\tau(n_j)$ on dyadic scales. This yields a structure-versus-randomness principle: either the orbit exhibits divisor mixing, or it develops strong additive structure. In the latter case, we show, under a phase-rigidity hypothesis, that the orbit contains long near-arithmetic progressions along which $\tau(n)$ is essentially constant, which we call divisor ladders. Our main result reduces the asymptotic behavior of $a(x)$ to a single structural obstruction. Assuming an anti-concentration hypothesis that rules out energy-saturating divisor ladders, we obtain $a(x) \asymp x / \log x$. The paper also establishes several unconditional structural results, including that large values of $\tau(n)$ are negligible on dyadic scales and that any potential obstruction must occur at a single divisor scale $\tau(n) \asymp \log n$.

The threshold for linear independence of multiple zeta values in positive characteristic
math.NT


Bo-Hae Im, Hojin Kim, Tuan Ngo Dac

A fundamental conjecture formulated by Thakur in 2009, which has guided significant developments in function field arithmetic, asserts that multiple zeta values (MZV's) in positive characteristic of fixed weight are linearly independent over $\mathbb{F}_q$. In this paper we settle this conjecture by determining the precise threshold for this independence. We prove that linear independence holds for all weights up to 2q, while for weight 2q+1 we establish the existence of a unique and explicit $\mathbb{F}_q$-linear relation. This result provides the first counterexample to Thakur's conjecture. Our proof relies on a new connection between MZVs and Carlitz multiple polylogarithms over $\mathbb{F}_q$, generalizing a central result of [IKLNDP24]. We also introduce a modification of the algorithm from [ND21] that yields a weight-preserving operator acting on $\mathbb{F}_q$-linear relations, providing the algebraic framework for these results.

Cyclotomic Numbers of Order $q-1$ over $\mathbb{F}_{q^r}$
math.NT


Hayaki Kudo, Yuto Nogata

Let $q=p^n$, $r\in \mathbb{Z}_{\ge 2}$, $e=q-1$, and $k=\frac{q^r-1}{e}$. In this paper, we study the cyclotomic numbers $(a,b)_{q-1}$ over $\mathbb{F}_{q^r}$. We prove that $(a,b)_{q-1}\le \left\lceil \frac{k}{2}\right\rceil$ for all $0\le a,b\le q-2$ except when $q=2$ and $r\ge 3$. We also give sharper bounds for prime values of $r$, especially for $r=2$ and $r=3$.

Some results on naive transcendence in the ring of integers modulo infinitely large primes
math.NT


Toshiki Matsusaka, Shin-ichiro Seki

This paper presents various transcendence results in the ring of integers modulo infinitely large primes $\mathcal{A}$. In the ring $\mathcal{A}$, one can consider two notions of transcendence. One is based on the notion of finite algebraic numbers introduced by Rosen, while the other is transcendence in the naive sense. It is known that transcendence in the latter sense automatically implies transcendence in the former sense. In this paper, we strengthen results of Anzawa-Funakura and Luca-Zudilin by removing some of their assumptions and, in some cases, upgrading them to statements of naive transcendence. We also present several examples of naive transcendental numbers that do not seem to have appeared previously in the literature. Although we are not able to establish naive transcendence for certain numbers, we prove the irrationality of numbers such as $\log_{\mathcal{A}}(2)$ under the ABC conjecture.

Conditional Upper Bounds for Large Deviations and Moments of the Riemann Zeta Function
math.NT
math.PR


Louis-Pierre Arguin, Emma Bailey, Asher Roberts

Assuming the Riemann Hypothesis, we show that for $k>0$ $$ \frac{1}{T}\text{meas}\Big\{t\in [T,2T]:|\zeta(1/2+{\rm i} t)|>(\log T)^k\Big\}\leq C_k \frac{(\log T)^{-k^2}}{\sqrt{\log\log T}}, $$ where $C_k=\exp(e^{ck})$ for some absolute constant $c>0$. This implies that the $2k$-moments of $|\zeta|$ are bounded above by $C_k(\log T)^{k^2}$, recovering the bound of Harper. The proof relies on the recursive scheme of one of the authors with Bourgade and Radziwill (2020), and combines ideas of Soundararajan (2009) and Harper (2013).

On numerical semigroups with embedding dimension four
math.NT


Kazimierz Chomicz

We develop a geometric procedure for finding the Ap\'ery set of any numerical semigroup with embedding dimension four. We use this method to find the Frobenius numbers, genera, Betti elements, minimal presentations and catenary degrees of numerical semigroups generated by four consecutive squares and four consecutive triangular numbers.

A structure theorem for sets with doubling $4+\delta$
math.NT
math.CO


Yifan Jing, Akshat Mudgal

We prove a structural result for sets of integers with doubling at most $4 + \delta$, with $\delta>0$ sufficiently small. This generalises earlier work of Eberhard--Green--Manners which dealt with sets of integers with doubling strictly less than $4$, and makes progress towards a question of Green.

The local Langlands correspondence of essentially unipotent supercuspidal representations for disconnected reductive groups
math.RT
math.NT


Amoru Fujii

We construct the local Langlands correspondence of essentially unipotent supercuspidal representations under the framework of rigid inner forms and prove a certaion functoriality and compatibilities. In particular, we show the equivariance under automorphisms, which is stronger than the analogous result in [FOS20]. We also generalize this correspondence for disconnected reductive groups under a mild condition on the group structure. We expect to use this result for extension of the explicit local Langlands correspondence in [Kal21] for more general supercuspidal representations.

A local-global correspondence for perfectoid purity
math.AG
math.AC
math.NT


Ryo Ishizuka, Shou Yoshikawa

We introduce (lim-)perfectoid splitting, which is a global variant of (lim-)perfectoid purity. Our main result establishes a correspondence between the lim-perfectoid splitting of projective schemes and the lim-perfectoid purity of their Gorenstein section rings. As an application, we construct a new supply of examples of lim-perfectoid pure rings that go beyond the previously known complete intersection or splinter-type cases.

Mild Pro-$p$ Groups and Ordered Monoids
math.GR
math.NT


Ido Efrat

We prove a criterion for the mildness of a finitely presented pro-$p$ group $G$. It implies as a special case a cohomological mildness criterion via Massey products, generalizing results due to Schmidt and G\"artner. It subsumes Labute's non-singular circuit criterion. We further show connections with the triangle condition for the mildness of pro-$p$ right-angled Artin groups, due to Quadrelli, Snopce and Vannacci.

On the Fourier transform of regularized Bessel functions on complex numbers and Beyond Endoscopy over number fields
math.NT
math.CA
v5


Zhi Qi

In this article, we prove certain Weber-Schafheitlin type integral formulae for Bessel functions over complex numbers. A special case is a formula for the Fourier transform of regularized Bessel functions on complex numbers. This is applied to extend the work of A. Venkatesh on Beyond Endoscopy for $\mathrm{Sym}^2$ on $\mathrm{GL}_2$ from totally real to arbitrary number fields.

Random Diophantine Equations in the Primes
math.NT
v2


Philip Holdridge

We consider equations of the form $a_{1}x_{1}^{k}+...+a_{s}x_{s}^{k}$ and when they have solutions in the primes. We define an analogue of the Hasse principle for solubility in the primes (which we call the prime Hasse principle), and prove that, whenever $s\ge 3k+2$, this holds for almost all such equations. This is based on work of Br\"udern and Dietmann on the Hasse principle. We then prove some further results about prime solubility and the prime Hasse principle, including a partial converse, and some counterexamples. Of particular interest are counterexamples of degree 2, which show that the analogue of the Hasse-Minkowski theorem fails for prime solubility.

Smooth polynomials with several prescribed coefficients
math.NT
v5


László Mérai

Let $\mathbb{F}_q[t]$ be the polynomial ring over the finite field $\mathbb{F}_q$ of $q$ elements. A polynomial in $\mathbb{F}_q[t]$ is called $m$-smooth (or $m$-friable) if all its irreducible factors are of degree at most $m$. In this paper, we investigate the distribution of $m$-smooth (or $m$-friable) polynomials with prescribed coefficients. Our technique is based on character sum estimates on smooth (friable) polynomials, Bourgains's argument (2015) applied for polynomials by Ha (2016) and on double character sums on smooth (friable) polynomials.

Lax-Phillips orbit counting in higher rank
math.NT
v2


Alex Kontorovich, Christopher Lutsko

Given a discrete lattice, $\Gamma < \operatorname{SL}_m(\mathbb{R})$, and a base point $o \in \mathbb{R}^m$, let $N_\Gamma(T)$ denote the number of points in the orbit $o \cdot \Gamma $ whose (Euclidean) length is bounded by a growing parameter, $T$. We demonstrate an abstract spectral method \`a la Lax-Phillips, capable of obtaining strong asymptotic estimates for $N_\Gamma(T)$, and compare and contrast it with other methods.

Arithmetic Properties modulo powers of $2$ and $3$ for Overpartition $k$-Tuples with Odd Parts
math.NT
v2


Hirakjyoti Das, Manjil P. Saikia, Abhishek Sarma

Recently, Drema and N. Saikia (2023) and M. P. Saikia, Sarma, and Sellers (2023) proved several congruences modulo powers of $2$ for overpartition triples with odd parts. In this paper, we study further divisibility properties of overpartition $k$-tuples with odd parts using elementary means as well as properties of modular forms. In particular, we prove several congruences modulo multiples of $3$, and an infinite family of congruences modulo powers of $3$; we also prove some cases of a conjecture of Saikia, Sarma, and Sellers.

Arithmetic Properties of Generalized Cubic and Overcubic Partitions
math.NT
v2


Hirakjyoti Das, Saikat Maity, Manjil P. Saikia

We prove several congruences satisfied by the generalized cubic and generalized overcubic partition functions, recently introduced by Amdeberhan, Sellers, and Singh. We also prove infinite families of congruences modulo powers of $2$ and modulo $12$ satisfied by the generalized overcubic partitions, as well as some density results that they satisfy. We use both elementary $q$-series techniques as well as the theory of modular forms to prove our results.

On a remark of Serre
math.NT
v2


Katie Ahrens, Jon Grantham

Inspired by a remark of Serre, we extend the search for primes $p$ such that the maximum Hasse bound for the number of points on an elliptic curve over $\mathbb{F}_{p^5}$ is not achieved. We then give a list of all $q<10^{70}$ such that the Hasse bound is not achieved over $\mathbb{F}_{q}$. We explore the heuristics for how many such numbers should exist in each case. Finally, look at similar criteria for genus $2$ and $3$ curves.

Algorithmic aspects of Newman polynomials and their divisors
math.NT
v2


Musbahu Idris, Jean-Marc Sac-Épée

We study the problem of determining which integer polynomials divide Newman polynomials. In this vein, we first give results concerning the $8438$ known polynomials with Mahler measure less than $1.3$. We then exhibit a list of polynomials that divide no Newman polynomial. In particular, we show that a degree-10 polynomial of Mahler measure \text{approximately} 1.419404632 divides no Newman polynomial, thereby improving the best known upper bound for any universal constant $\sigma$, if it exists, such that every integer polynomial of Mahler measure less than $\sigma$ divides a Newman polynomial. Finally, letting $l(x)$ denote Lehmer's polynomial, we explicitly construct Newman polynomials divisible by $l(x)^2$ with degrees up to $150$, and show that no Newman polynomial is divisible by $l(x)^3$ up to degree $160$.

Torsion points on $\rm{GL}_2$-type abelian varieties
math.NT
v3


Jessica Alessandrì, Nirvana Coppola

It is well known that the rational torsion of an abelian variety defined over a number field injects into the reduction modulo any sufficiently large prime, so the order of the torsion group divides the greatest common divisor of the sizes of points on the reduction at each prime. Drawing inspiration from Katz's Inventiones paper (1981), we investigate the converse to this for abelian varieties of $\rm GL_2$-type and exhibit a conjectural list of possible torsion orders for modular abelian varieties over $\mathbb Q$ of dimension up to $5$.

Relating Mahler measures and Dirichlet $L$-values: new evidence for Chinburg's conjectures
math.NT
v2


David Hokken, Mahya Mehrabdollahei, Berend Ringeling

Let $\chi_{-f}$ be the odd quadratic Dirichlet character of conductor $f$, and let $\mathrm{m}(P)$ denote the Mahler measure of a polynomial $P$. In 1984, Chinburg conjectured that for any such $\chi_{-f}$ there exist an integral bivariate rational function $P$ (and, in the strong form, an integral polynomial) such that $\mathrm{m}(P)$ is a rational multiple of $L'(\chi_{-f},-1)$. The strong form of the conjecture was previously known to hold for $18$ values of $f$. We double the number of numerical examples, giving $8$ new instances of the strong and $18$ new instances of the weak conjecture. Our examples arise from an explicit approach, which also captures almost all of the previously known results, and is based on work of Boyd and Rodriguez-Villegas. Moreover, we prove Chinburg's weak conjecture if we allow cyclotomic coefficients.

On canonicity for integral models of Shimura varieties with hyperspecial level
math.NT
math.AG
v2


Keerthi Madapusi, Alex Youcis

We give a new definition -- and in some cases, a new construction -- of integral canonical models of Shimura varieties that uses the notion of an aperture appearing in work of Gardner--Madapusi on some conjectures of Drinfeld. This applies to Shimura varieties of pre-abelian type at odd primes of hyperspecial level, recovering and extending previous work of Kisin, Kim--Madapusi and Imai--Kato--Youcis, but also to exceptional Shimura varieties for large enough primes. The characterization in the exceptional case is \emph{a priori} different from the one recently shown by Bakker--Shankar--Tsimerman, and recovers many of their results, such as the existence of prime-to-$p$ Hecke operators, the non-emptiness of the $\mu$-ordinary stratum and the theory of the canonical lift. In fact, we give a uniform proof of the non-emptiness of \emph{all} possible Newton strata, and of the non-emptiness of Ekedahl--Oort strata and central leaves as well. An important ingredient in the proofs is a generalization of Tate's full faithfulness theorem for $p$-divisible groups to the context of apertures. This leads to a mapping property for the integral canonical model that characterizes maps into it from all normal, flat and excellent schemes over $\mathbb{Z}_{(p)}$.

Lattice point visibility along powers of polynomials
math.NT
v2


Abraham Lobsenz, Tristan Phillips

We study lattice point visibility along polynomial lines of sight and prove the Visibility Density Conjecture of Chaubey and Pandey for a large class of polynomials.

Unbounded logarithmic limsup in Erd\H{o}s problem 684
math.NT
math.CO
v2


Ji Ho Bae

For $0\le k\le n$, write $\binom nk=uv$ where the primes dividing $u$ are at most $k$ and the primes dividing $v$ exceed $k$, and let $f(n)$ be the least $k$ with $u>n^2$; Erd\H{o}s problem 684 asks for bounds on $f(n)$. We resolve the problem at the order level. By a short-multiplier construction $n_M=tL_M-1$, where $L_M=\operatorname{lcm}(1,\ldots,M)$ and $t$ is a multiplier of size $\exp(o(M))$ extracted from a Fourier sieve, we prove that for every fixed $C>1$ there exist integers $n$ with $$ f(n)>(C-o(1))\log n, $$ hence $$ \limsup_{n\to\infty}\frac{f(n)}{\log n}=\infty. $$ We thus refute the widely expected upper bound $f(n)\ll\log n$ and place the order of $f(n)$ strictly above $\log n$ infinitely often. A matching polylogarithmic upper bound $f(n)\ll(\log n)^2$ is known by Alexeev, Putterman, Sawhney, Sellke, and Valiant (arXiv:2603.29961). The reduction of the multiplier sieve to a dyadic fixed-$\Omega$ arithmetic-progression estimate, including a $Q_M=M!/L_M$ box parametrization, a local harmonic-height cap, and an exact-$a$ product-shell extraction, is new. The required estimate uses Timofeev's mean-in-progressions framework together with a Burgess-based mod-$p$ saving on the relevant prime band.

A virtually nilpotent group whose Green series is not D-finite
math.GR
math.CO
math.NT
v2


Corentin Bodart

We provide the first example of virtually nilpotent group, with a specific generating set, for which the Green series (sometimes called cogrowth series) is not $D$-finite. The proof relies on an arithmetical miracle, and the study of the subword complexity of a multiplicative sequence coming out of it.

Intersections of the automorphism and the Ekedahl-Oort strata in $M_2$
math.AG
math.NT
v2


Alvaro Gonzalez-Hernandez

We compute the intersections between the automorphism strata and the pullback by the Torelli map of the Ekedahl-Oort strata inside the moduli space of genus two curves. We first describe explicitly which possible automorphism groups a genus two curve can have over a field of positive characteristic, and parametrise the families of curves with a prescribed automorphism group. Then, we describe an algorithm to compute the strata of genus two curves whose Jacobian variety has a fixed Ekedahl-Oort type. Finally, we compute the dimension and number of irreducible components of the intersections between the strata.

Recurrence Time for Finite Quantum Systems
quant-ph
math.NT
v2


Chaitanya Gupta, Anthony J. Short

We study the time it takes for all states of a finite quantum system to return simultaneously to their original configuration. In particular, we define the recurrence time for a quantum system to be the time at which all time-evolved states are close to their initial configuration, and at least one state has deviated significantly during this interval. Considering finite-dimensional quantum systems evolving unitarily, we find bounds on this notion of recurrence time, for continuous time and discrete time, by using Dirichlet's approximation theorem. We show how the problem of finding a bound on recurrence time can be related to approximating the difference of real numbers by rationals. We present a mathematical result on the latter, which we then use to obtain tighter bounds on recurrence time.

Generalized Howe curves of genus 4, 5, and 6 with completely decomposable Jacobians
math.AG
math.NT
v2


Ryo Ohashi

Superspecial curves are important objects in number theory and algebraic geometry, and the existence in genus $g \geq 4$ remains an open problem for all but finitely many characteristics $p > 0$. As a computational approach to this problem, Kudo-Harashita-Howe (2020) showed that a superspecial curve of genus 4 exists in each characteristic $p$ with $7 < p < 20000$. Their method restricted attention to a specific class of curves, known as Howe curves, for which superspeciality is reduced to those of curves of genus at most 2. In this paper, we focus on a more specific class of curves, namely Howe curves whose Jacobians decompose into a product of four elliptic curves. By restricting our attention to such curves, the superspeciality reduces to the supersingularity of elliptic curves, which enables us to construct a superspecial curve of genus 4 more efficiently than Kudo-Harashita-Howe's method. As our first main result, we confirmed by computer the existence of such superspecial curves of genus 4 in characteristics $p$ with $20000 < p < 10^6$. Using a similar approach, we also propose constructions of superspecial curves of genera 5 and 6 from only supersingular elliptic curves. Furthermore, computational experiments establish the existence of superspecial curves of genus 5 (resp. genus 6) in characteristics $p$ with $13 < p < 10^5$ (resp. $7 < p < 10^5$).

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8
math.MG
cs.AI
cs.LO
math.NT
v2


Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska

In 2016, Viazovska famously solved the sphere packing problem in dimension $8$, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain.