{"id":"palomar/PALOMAR-2026-08-26-000004","url":"https://github.com/JD-Jones-ASES/fs-formal/tree/4e796565301b1425c53e807a6edf408535b2e922","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000004-v1.json","repo":"https://github.com/JD-Jones-ASES/fs-formal","tags":["math.CO","math.NT","msc:11B30","msc:11B75","additive-combinatorics","number-theory","lean","furstenberg-sarkozy"],"score":0,"title":"JD-Jones-ASES/fs-formal","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization of an explicit construction for the Furstenberg-Sárközy problem. If D(N) is the largest size of a subset of {1,...,N} with no nonzero square difference, the development proves that an explicit eleven-block constant alphaInf is at most liminf log D(N)/log N, that every exponent below alphaInf holds eventually pointwise, and that 0.7537 < alphaInf. The proof includes the finite certificates, the composite even-digit lift, CRT gluing, asymptotic passage, and kernel-checked numerical inequalities. This strictly improves Krachun's preceding explicit exponent…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-26","reactions":{},"formalized":true,"formalizes":[{"title":"An improved lower bound for the Furstenberg-Sárközy problem","identifier":"https://github.com/JD-Jones-ASES/fs-lower-bound/tree/c2c06875ee4544e069e8da16564ee429d870a13e","relationship":"formalizes"}]}