Local Factors in the BSD Conjecture: A Unified Statistical View
David Kurniadi Angdinata, Kenny Lau, Ken Ono, Ashvin Swaminathan, Sameera Vemulapalli
math.NT
Oct 7, 2026 · v1
TL;DR
All theorems and lemmas were autoformalized in Lean by AxiomProver (21 formal targets), with a public repository checked by the Lean comparator.
Abstract
For elliptic curves $E/\mathbb{Q}$ in short Weierstrass form \[ E=E(a_4,a_6): y^2=x^3+a_4x+a_6, \] we derive a multivariable Euler product generating function which encodes the Tamagawa product $Tam(E)=\prod_p c_p(E)$. Using this generating function, we compute limiting distributions, exact covariances, and moment and tail bounds for four important statistics on the Tamagawa number; for example we show that more than half of all curves in this height ordering have trivial Tamagawa product, about $42.2\%$ have exactly one prime with nontrivial local Tamagawa number, and only about $6.8\%$ have exactly two such primes. The product is obtained by specializing an Euler product indexed by local reduction data that we derive from Tate's algorithm. The results in this paper were autoformalized in Lean by AxiomProver.
Problem
The goal is to determine the statistical distribution of the Tamagawa product Tam(E) = ∏ c_p(E) for elliptic curves y^2 = x^3 + a_4x + a_6 ordered by naive height. This quantity appears in the Birch–Swinnerton-Dyer conjecture.
Approach
The authors derive a multivariable Euler product generating function, indexed by local reduction data from Tate's algorithm, that encodes the Tamagawa product. Statistics are first truncated to finite sets of primes and then extended to all primes. Normal-family (Vitali–Montel) arguments are used to extract coefficients. All results were autoformalized in Lean by AxiomProver.
Results
The paper obtains limiting distributions, exact covariances, and moment and tail bounds for four Tamagawa statistics. More than half of curves have trivial Tamagawa product, about 42.2% have exactly one prime with a nontrivial local Tamagawa number, and about 6.8% have exactly two. The Lean formalization of 21 targets is reported as verified.
