Erdős 1180: representing residues as sums of modular inverses with small denominators
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-12-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-12-000005/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-12-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'