Number Theory

Formulated in 1985 by Joseph Oesterlé and David Masser as an arithmetic distillation of Szpiro's conjecture on elliptic curves, the abc conjecture makes a deceptively simple claim about coprime triples with a + b = c: the three numbers cannot all be built from many repeated small primes at once, so c can only rarely exceed rad(abc)^(1+ε). Dorian Goldfeld called it 'the most important unsolved problem in Diophantine analysis,' and for good reason — a single proof would cascade through number theory, delivering Fermat's Last Theorem for all large exponents almost for free, along with Roth's theorem, the Mordell–Faltings theorem, the Fermat–Catalan conjecture, infinitely many non-Wieferich primes, and all but finitely many counterexamples to Beal's conjecture. Since 2012 Shinichi Mochizuki has claimed a proof via inter-universal Teichmüller theory, published in 2021, but the community has not accepted it: in 2018 Peter Scholze and Jakob Stix identified a gap they regarded as fatal. A precise formal statement gives everyone a shared, machine-checkable target around which to organize verified progress.

Motivation

An $(n,d,\lambda)$-graph is a $d$-regular graph on $n$ vertices in which every eigenvalue of the adjacency matrix other than the top eigenvalue $d$ has absolute value at most $\lambda$. Graphs of this kind with $\lambda$ small compared with $d$ are expanders. They are used in derandomization, error-correcting codes, sorting networks and many other constructions in theoretical computer science. A Ramanujan graph achieves $\lambda\le 2\sqrt{d-1}$, which is asymptotically optimal.

The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (LPS, 1988) exist only for special vertex counts, such as $q(q^2-1)/2$ for a prime $q$ or the size of a quaternion group modulo $m$. N. Alon, in Explicit expanders of every degree and size (arXiv:2003.11673, 2020; Combinatorica 41, 2021), asks for explicit $(n,d,\lambda)$-graphs with $\lambda\le(2+o(1))\sqrt d$ for every degree $d$ and every number of vertices $n$. His Proposition 1.1 builds such graphs out of LPS graphs, and one ingredient is purely arithmetic. If the available vertex counts of an LPS family are dense enough, so that for every large $n$ one is within a factor $1+o(1)$ of $n$, then a few vertices can be added or removed while keeping the spectral bound.

This mission formalizes that ingredient, Lemma 2.2 of the paper (p. 7). It concerns the vertex counts of the LPS graphs $H(p,q_1^sq_2^t)$ for two fixed primes $q_1,q_2$ and all exponents $s,t\ge1$. With $q_1,q_2$ fixed, the construction needs no large primes, which is why Proposition 1.1 is strongly explicit for every fixed degree.

Setting

Fix natural numbers $q_1,q_2$. For natural numbers $s,t$ define the LPS vertex count

When $q_1,q_2$ are distinct primes congruent to $1$ modulo $4p$ and $s,t\ge1$, this is the number of vertices of the LPS Cayley graph $H(p,q_1^sq_2^t)$ (§2.3, p. 6). Lemma 2.2 itself only requires $q_1,q_2$ to be distinct primes. Both fractions are integers, because $q(q-1)(q+1)$ is a product of three consecutive integers.

The proof uses the real number $\alpha=\log q_1/\log q_2$, and the fractional part $\{x\}=x-\lfloor x\rfloor\in[0,1)$, written $x \bmod 1$ in the paper.

Formalization targets

Goal: Lemma 2.2

For distinct primes $q_1,q_2$ there is a function $g:\mathbb N\to\mathbb R$ with $g(n)=o(n)$ such that for all sufficiently large $n$ there are integers $s,t\ge1$ with

Equivalently, the ratio between consecutive elements of $\{Q(q_1,q_2,s,t):s,t\ge1\}$ tends to $1$. The statement fixes no rate for $g$, matching the paper's $o(n)$.

Milestones, in the order the proof of Lemma 2.2 uses them (p. 7)

1. For distinct primes $q_1,q_2$, $\alpha=\log q_1/\log q_2$ is irrational.
2. For irrational $\alpha$ and every $\delta>0$ there is $k_1\ge1$ with $0<\{k_1\alpha\}<\delta$.
3. For distinct primes $q_1,q_2$ and every $\mu>0$ there are $k_1\ge1$, $k_2\ge0$ with

4. For distinct primes, $\mu>0$ and $k_1\ge1$, if $1\le q_1^{k_1}/q_2^{k_2}\le1+\mu$, then for $s>k_1$ and $t\ge1$

Significance

The result. Lemma 2.2 is the step of Proposition 1.1 that turns a family of Ramanujan graphs with sparse vertex counts into a family whose vertex counts approximate every large $n$ up to a factor $1+o(1)$. The deviation from $n$ can then be absorbed by the general packing argument of §2.1 of the paper. Without it, the construction would have to search for large primes depending on $n$, and the result would be explicit but not strongly explicit.

The formalization. The lemma is proved in the paper, in one paragraph. To our knowledge no machine-checked proof exists, and the platform has no statement of it. The only related platform item is the irrationality of $\log 2/\log 3$, the case $q_1=2$, $q_2=3$ of milestone 1. Formalizing the lemma requires a quantitative inhomogeneous step that the paper leaves implicit ("implying the desired result"). Its last sentence also contains a misprint that the formalization corrects (see below). The Diophantine milestones 1–3 are reusable for any argument about the multiplicative density of $\{q_1^a q_2^b\}$, for instance the ratio of consecutive elements of $\{2^a3^b\}$.

Difficulty

Each milestone is short. The difficulty is in making the paper's last sentence ("implying the desired result") into a proof. Taking $s$ or $t$ large separately does not work: changing $s$ or $t$ by one multiplies $Q$ by $q_1^3$ or $q_2^3$, a fixed factor larger than $1$, so the values obtained by varying one exponent leave gaps of a constant ratio. The bound must hold for every large $n$, not just along a subsequence, and the exponents must stay positive throughout. Milestone 2 is the classical fact that the multiples of an irrational number are dense modulo $1$. It needs a pigeonhole argument, not just the irrationality.

Formalization scope

• Representation. $Q$ is a natural-number-valued Lean definition given by the explicit formula above, not the cardinality of a quaternion group. The graph-count interpretation needs the section's congruence conditions on $p,q_1,q_2$; Lemma 2.2 is an arithmetic statement for all distinct primes $q_1,q_2$. Every use of $Q$ in the theorems has positive $s,t$, so natural-number subtraction $s-1$ is exact, and the division by $2$ is exact since $q(q-1)(q+1)$ is even. Ratios and the bound $n+g(n)$ are computed in $\mathbb R$ after casting. The logarithm is Real.log, and the fractional part is Int.fract.
• o(n). The paper writes $n\le Q\le n+o(n)$ for every large $n$. The goal states it literally: $\exists g,\ g=o(n)$ (Mathlib IsLittleO along atTop) and, eventually in $n$, $\exists s,t\ge1$ with $n\le Q\le n+g(n)$. This is equivalent to the form "for every $\mu>0$, every large $n$ has $s,t\ge1$ with $n\le Q\le(1+\mu)n$". The paper's proof yields the second form, with the factor $(1+\mu)^3$ for arbitrary $\mu$.
• Misprint. The paper's last sentence compares $Q(q_1,q_2,s,t)$ with $Q(q_1,q_2,s-k_1,t-k_2)$ for $s,t\ge\max\{k_1,k_2\}$. As printed the ratio is $q_1^{3k_1}q_2^{3k_2}$, which is not close to $1$. Milestone 4 uses the intended pair $(s-k_1,t+k_2)$, with $s>k_1$ so that $s-k_1\ge1$.
• Ruling out a trivial reading. The lower bound $n\le Q(q_1,q_2,s,t)$ alone holds for every $n$ by taking $s$ large. The content of the goal is the upper bound with a sublinear excess, and $s,t$ must be positive. In milestone 3 the condition $k_1\ge1$ excludes the trivial witness $k_1=k_2=0$.
• Out of scope. The derivation of $Q$ as the vertex count of $H(p,q_1^sq_2^t)$ (Hensel's lemma and the Chinese remainder theorem, pp. 6–7), Theorem 2.1 (the LPS graphs are Ramanujan, cited from Lubotzky–Phillips–Sarnak), Proposition 1.1, the §2.1 packing argument, and every running-time ("explicit", "strongly explicit") claim.
• Infrastructure. Only Mathlib is needed: unique factorization for milestone 1, Int.fract and a pigeonhole or Dirichlet-approximation argument for milestone 2, and real exponentiation and asymptotics for the goal. Contributions of alternative proofs of milestone 2, for instance via Mathlib's Dirichlet approximation theorem, are welcome.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673 , https://doi.org/10.1007/s00493-020-4429-x
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8