This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.

We prove sharp smoothing properties of the averaging operator defined by convolution with a measure on a smooth nondegenerate curve $\gamma $ in $\mathbb R^d$, $d\ge 3$. Despite the simple geometric structure of such curves, the sharp smoothing estimates have remained largely unknown except for those in low dimensions. Devising a novel inductive strategy, we obtain the optimal $L^p$ Sobolev regularity estimates, which settle the conjecture raised by Beltran–Guo–Hickman–Seeger [1]. Besides, we show the sharp local smoothing estimates on a range of p for every $d\ge 3$. As a result, we establish, for the first time, nontrivial $L^p$ boundedness of the maximal average over dilations of $\gamma $ for $d\ge 4$.

Building upon the pioneering work of Merle, Raphaël, Rodnianski and Szeftel [67, 68, 69], we construct exact, smooth self-similar imploding solutions to the 3D isentropic compressible Euler equations for ideal gases for all adiabatic exponents $\gamma>1$. For the particular case $\gamma =\frac 75$ (corresponding to a diatomic gas – for example, oxygen, hydrogen, nitrogen), akin to the result [68], we show the existence of a sequence of smooth, self-similar imploding solutions. In addition, we provide simplified proofs of linear stability [67] and nonlinear stability [69], which allow us to construct asymptotically self-similar imploding solutions to the compressible Navier-Stokes equations with density independent viscosity for the case $\gamma =\frac 75$. Moreover, unlike [69], the solutions constructed have density bounded away from zero and converge to a constant at infinity, representing the first example of singularity formation in such a setting.

We study the locally analytic vectors in the completed cohomology of modular curves and determine the eigenvectors of a rational Borel subalgebra of $\mathfrak {gl}_2(\mathbb {Q}_p)$. As applications, we prove a classicality result for overconvergent eigenforms of weight 1 and give a new proof of the Fontaine–Mazur conjecture in the irregular case under some mild hypotheses. For an overconvergent eigenform of weight k, we show its corresponding Galois representation has Hodge–Tate–Sen weights $0,k-1$ and prove a converse result.

In their book Subgroup Growth, Lubotzky and Segal asked: What are the possible types of subgroup growth of the pro-$p$ group? In this paper, we construct certain extensions of the Grigorchuk group and the Gupta–Sidki groups, which have all possible types of subgroup growth between $n^{(\log n)^{2}}$ and $e^{n}$. Thus, we give an almost complete answer to Lubotzky and Segal’s question. In addition, we show that a class of pro-$p$ branch groups, including the Grigorchuk group and the Gupta–Sidki groups, all have subgroup growth type $n^{\log n}$.

Let f be an $L^2$-normalized holomorphic newform of weight k on $\Gamma _0(N) \backslash \mathbb {H}$ with N squarefree or, more generally, on any hyperbolic surface $\Gamma \backslash \mathbb {H}$ attached to an Eichler order of squarefree level in an indefinite quaternion algebra over $\mathbb {Q}$. Denote by V the hyperbolic volume of said surface. We prove the sup-norm estimate

$$\begin{align*}\| \Im(\cdot)^{\frac{k}{2}} f \|_{\infty} \ll_{\varepsilon} (k V)^{\frac{1}{4}+\varepsilon} \end{align*}$$

with absolute implied constant. For a cuspidal Maaß newform $\varphi $ of eigenvalue $\lambda $ on such a surface, we prove that

$$\begin{align*}\|\varphi \|_{\infty} \ll_{\lambda,\varepsilon} V^{\frac{1}{4}+\varepsilon}. \end{align*}$$

We establish analogous estimates in the setting of definite quaternion algebras.

Define the Collatz map ${\operatorname {Col}} \colon \mathbb {N}+1 \to \mathbb {N}+1$ on the positive integers $\mathbb {N}+1 = \{1,2,3,\dots \}$ by setting ${\operatorname {Col}}(N)$ equal to $3N+1$ when N is odd and $N/2$ when N is even, and let ${\operatorname {Col}}_{\min }(N) := \inf _{n \in \mathbb {N}} {\operatorname {Col}}^n(N)$ denote the minimal element of the Collatz orbit $N, {\operatorname {Col}}(N), {\operatorname {Col}}^2(N), \dots $. The infamous Collatz conjecture asserts that ${\operatorname {Col}}_{\min }(N)=1$ for all $N \in \mathbb {N}+1$. Previously, it was shown by Korec that for any $\theta> \frac {\log 3}{\log 4} \approx 0.7924$, one has ${\operatorname {Col}}_{\min }(N) \leq N^\theta $ for almost all $N \in \mathbb {N}+1$ (in the sense of natural density). In this paper, we show that for any function $f \colon \mathbb {N}+1 \to \mathbb {R}$ with $\lim _{N \to \infty } f(N)=+\infty $, one has ${\operatorname {Col}}_{\min }(N) \leq f(N)$ for almost all $N \in \mathbb {N}+1$ (in the sense of logarithmic density). Our proof proceeds by establishing a stabilisation property for a certain first passage random variable associated with the Collatz iteration (or more precisely, the closely related Syracuse iteration), which in turn follows from estimation of the characteristic function of a certain skew random walk on a $3$-adic cyclic group $\mathbb {Z}/3^n\mathbb {Z}$ at high frequencies. This estimation is achieved by studying how a certain two-dimensional renewal process interacts with a union of triangles associated to a given frequency.

In this paper, we consider the defocusing nonlinear wave equation $-\partial _t^2u+\Delta u=|u|^{p-1}u$ in $\mathbb {R}\times \mathbb {R}^d$. Building on our companion work (Self-similar imploding solutions of the relativistic Euler equations, arXiv:2403.11471), we prove that for $d=4, p\geq 29$ and $d\geq 5, p\geq 17$, there exists a smooth complex-valued solution that blows up in finite time.

We determine the density of integral binary forms of given degree that have squarefree discriminant, proving for the first time that the lower density is positive. Furthermore, we determine the density of integral binary forms that cut out maximal orders in number fields. The latter proves, in particular, an ‘arithmetic Bertini theorem’ conjectured by Poonen for ${\mathbb {P}}^1_{\mathbb {Z}}$.

Our methods also allow us to prove that there are $\gg X^{1/2+1/(n-1)}$ number fields of degree n having associated Galois group $S_n$ and absolute discriminant less than X, improving the best previously known lower bound of $\gg X^{1/2+1/n}$.

Finally, our methods correct an error in and thus resurrect earlier (retracted) results of Nakagawa on lower bounds for the number of totally unramified $A_n$-extensions of quadratic number fields of bounded discriminant.

Multiples zeta values and alternating multiple zeta values in positive characteristic were introduced by Thakur and Harada as analogues of classical multiple zeta values of Euler and Euler sums. In this paper, we determine all linear relations between alternating multiple zeta values and settle the main goals of these theories. As a consequence, we completely establish Zagier–Hoffman’s conjectures in positive characteristic formulated by Todd and Thakur which predict the dimension and an explicit basis of the span of multiple zeta values of Thakur of fixed weight.