A Lean formalization of the Erdős discrepancy theorem
A formalization in Lean 4 and Mathlib of the Erdős discrepancy theorem, proved by Terence Tao in 2015: for every sequence f(1), f(2), … of signs ±1 and every C there are d ≥ 1 and n with |f(d) + f(2d) + ⋯ + f(nd)| > C, so every ±1 sequence has unbounded discrepancy along homogeneous arithmetic progressions. This is the original ±1 formulation, Corollary 1.2 of Tao's paper; its Hilbert-space-valued Theorem 1.1 is not formalized. The proof follows the architecture of Tao's argument: a Fourier-analytic reduction from a sequence of bounded discrepancy to a stochastic completely multiplicative…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-29-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-29-000002/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-09-29-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'