{"id":"palomar/PALOMAR-2026-10-22-000029","url":"https://github.com/gdahia/SzemerediWithRandomDifferences/tree/ec1328dcdb8efe9c683124546358173c267b9522","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000029-v1.json","repo":"https://github.com/gdahia/SzemerediWithRandomDifferences","tags":["math.CO","math.NT","msc:11B25","msc:11B30","msc:05D40","additive-combinatorics","szemeredi-theorem","random-sets","lean-formalization"],"score":0,"title":"Szemerédi's theorem with random differences","trust":"high","domain":"math.CO","source":"palomar","authors":["Gabriel Dahia"],"reviews":0,"subject":"math.CO","summary":"Lean 4 formalization of the main result of the preprint \"Szemerédi's theorem with random differences and arithmetic Kakeya\" by Gabriel Dahia (arXiv:2610.18859), a threshold for Szemerédi's theorem with random differences. For c = 1/100, k ≥ 3, δ > 0 and p ≥ C n^(-c / log log k), where C is a value of the Ackermann function depending on k and δ, a p-random set D of differences in {1, …, n} has the following property with probability at least 1 - exp(-n^(1 - c / log log k)): every subset of {1, …, n} with at least δn elements contains a k-term arithmetic progression with common difference in…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Szemerédi's theorem with random differences and arithmetic Kakeya","identifier":"arXiv:2610.18859","relationship":"formalizes"},{"title":"On the arithmetic Kakeya conjecture of Katz and Tao","identifier":"arXiv:1712.02108","relationship":"formalizes"}]}