The density Hales–Jewett theorem and Szemerédi's theorem
A Lean 4 formalization of the density Hales–Jewett theorem: for every finite alphabet α and every density δ > 0, all sufficiently large n have the property that any set of at least δ·|α|^n words of length n over α contains a combinatorial line. The basis for the formalization is the combinatorial proof of Dodos, Kanellopoulos, and Tyros. As a consequence, we also formalize Szemerédi's theorem on the integers: for every k ≥ 3 and δ > 0, the following holds for all sufficiently large n. Any subset of {0, …, n−1} of size at least δ·n contains a nonconstant arithmetic progression of length k.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-06-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-06-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-09-06-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'