Papers With

← All papers
First page of Joint Linnik problems

Joint Linnik problems

Valentin Blomer, Farrell Brumley, Maksym Radiwiłł

math.NT Mar 5, 2026 · v1
formalization number-theory
Read PDF arXiv abstract Code
TL;DR
Lean 4 is used to formalize the numerically critical Lemma 7.2, a polynomial positivity construction used in the Hecke eigenvalue distribution argument.
Abstract
We prove a conjecture of Michel–Venkatesh on joinings of distinct Linnik problems, in the setting of simultaneous quaternionic embeddings of imaginary quadratic fields having sufficiently many small split primes. This splitting condition is known to hold for all but $O((\log\log X)^{1 + o(1)})$ discriminants up to $X$. We also treat a non-equivariant form of this conjecture proposed by Aka–Einsiedler–Shapira, which in particular applies to the classical Gauss construction joining Linnik points on the sphere with CM points on the modular surface.
Problem

The paper addresses the Michel–Venkatesh conjecture on joinings of distinct Linnik problems, that is, simultaneous equidistribution of quaternionic embeddings of imaginary quadratic fields. It also treats a non-equivariant variant due to Aka–Einsiedler–Shapira, which covers Gauss's orthogonal complement construction. Earlier results relied on GRH and on cuspidality of the test functions.

Approach

Via the Weyl criterion, the problem is reduced to bounds on period sums. These are attacked with mollifiers guided by the Waldspurger formula, Cauchy–Schwarz, Parseval and spectral theory. The argument also uses twisted moments of L-functions, the distribution of Hecke eigenvalues via symmetric power lifts with constructed positive polynomials, and character sums over primes under zero-free conditions. The numerically critical Lemma 7.2 is formalized in Lean 4.

Results

The conjecture is proved for quaternionic varieties at almost maximal level, assuming only a splitting condition on small primes that is roughly equivalent to the absence of Siegel zeros. This condition holds for all but O((log log X)^{1+o(1)}) discriminants up to X, and the continuous spectrum is also handled.