{"id":"palomar/PALOMAR-2026-10-12-000005","url":"https://github.com/linrock/math-proofs/tree/ba96303b34a95ac458958c1eb0bbdee54733484a/erdos-1180","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-12-000005-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.NT","math.CO","msc:11B13","msc:11T23","number-theory","modular-inverses","lean-formalization"],"score":0,"title":"Erdős 1180: representing residues as sums of modular inverses with small denominators","trust":"high","domain":"math.NT","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.NT","summary":"A complete Lean 4 proof of Erdős problem 1180 and its quantitative variants on representing every residue modulo a prime p as a sum of at most C(ε) modular inverses n⁻¹ (mod p) with 1 ≤ n ≤ p^ε and gcd(n, p) = 1. Formalizing Glibichuk's 8-fold bilinear covering theorem via additive energy and Cauchy–Davenport together with an inductive asymmetric two-block prime-reciprocal construction, this development proves the affirmative existence theorem for all ε > 0 and all primes p, the discrete large-prime bound C_asymp(ε) ≤ 8(⌊1/ε⌋ + 1)² = (8 + o(1))ε⁻² (and ≤ 32ε⁻² uniformly on (0, 1]), the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-12","reactions":{},"formalized":true,"formalizes":[{"title":"Combinatorial properties of sets of residues modulo a prime and the Erdős–Graham problem","identifier":"https://doi.org/10.1007/s11006-006-0040-8","relationship":"formalizes"},{"title":"Additive combinatorics over finite fields: new results and applications","identifier":"","relationship":"formalizes"},{"title":"On a question of Erdős and Graham","identifier":"https://doi.org/10.1007/s00013-002-8270-z","relationship":"adapts"}]}