The exponent $3/4$ for the exceptional sets of the equations $K/n=1/x+1/y+1/z$
Dmytro Trybushnyi
math.NT
Nov 10, 2026 · v1
TL;DR
Every lemma, proposition and theorem, with all explicit constants, is formalized in Lean 4 with Mathlib, plus an audit file restating headline results.
Abstract
For $K\ge4$ let $E_K(N)$ be the number of integers $2\le n\le N$ for which $K/n=1/x+1/y+1/z$ has no solution in positive integers; $K=4$ is the Erdős-Straus equation. We prove that $E_K(N)\le N\exp(-c((\log N)^3/K)^{1/4})$ with absolute constants $c,B>0$, uniformly for $4\le K\le(\log N)^3/B$. This improves the exponent $2/3$ of Vaughan's bound of 1970. The bound is non-trivial for $K$ up to a constant times $(\log N)^3$, which is, up to a factor $(\log\log N)^{2+o(1)}$, the scale at which, by work of Pomerance and Weingartner, exceptional primes become common. The sieve is combinatorial: a truncated inclusion-exclusion over the classes of parametric solutions, whose second moment is the partition function of a two-copy polymer gas, bounded by a real form of the Kotecký-Preiss criterion. Averaging over the residue classes of the small primes gives the family its full mass, and summing each cluster in a random order bounds the cluster sums. Since a divisor of an exception is an exception, nothing about the small primes themselves is needed, and the sieve can use the classes of the whole family of parametric solutions, one triple per class. All constants are explicit, and the whole proof has been checked in the proof assistant Lean 4.
Problem
For K>=4, E_K(N) counts integers n<=N for which K/n=1/x+1/y+1/z has no positive integer solution; K=4 is the Erdős–Straus equation. Since 1970 the best bound was Vaughan's, with exponent 2/3 in the exponential saving.
Approach
A combinatorial sieve uses truncated inclusion-exclusion over classes of parametric (Type II) solutions. Its second moment is the partition function of a two-copy polymer gas, bounded by a real-valued Kotecký–Preiss criterion. Averaging over residue classes of small primes gives the family full mass, and the fact that divisors of exceptions are exceptions removes any need for information about the small primes. The entire proof, with explicit constants, is formalized in Lean 4 (v4.22.0) with Mathlib and replayed by lean4checker; an audit file restates the main theorems using only Mathlib definitions.
Results
E_K(N) <= N exp(-c((log N)^3/K)^{1/4}) with c=1/6144, uniformly for 4<=K<=(log N)^3/B, improving the exponent from 2/3 to 3/4. For K=4 and N>=2^{2^{64}}, E_4(N) <= N exp(-(log N)^{3/4}/8689). All statements are checked by Lean's kernel.
