{"id":"palomar/PALOMAR-2026-09-17-000003","url":"https://github.com/JD-Jones-ASES/ns-lean/tree/035e9b0c147630e35631e4401433660f695d1fba","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-17-000003-v1.json","repo":"https://github.com/JD-Jones-ASES/ns-lean","tags":["math.NT","math.CO","msc:11T55","msc:11B30","msc:05B40","finite-fields","polynomials","combinatorics","lean-formalization"],"score":0,"title":"ns-lean: Naslund's Conjecture 13 is false at q = 3, k = 2, for every n congruent to 0 mod 4 with n >= 8","trust":"high","domain":"math.NT","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof that square-difference-free subsets of the polynomials of degree below n over F_3 can be larger than 3^(3n/4). Call A square-difference-free when no two of its elements differ by a nonzero square, and let D_3(n) be the largest size of such a set inside P_{3,n}. A ten-word code S in F_3^4, in which no two words differ by a vector with every coordinate in {0, 1}, drives a lift that carries a square-difference-free subset of P_{3,m} to one of P_{3,m+8} with 810 times as many elements. Iterating it from the bases {0} and B_4 = {a T^3 + b T + c (1 - T^2)} gives…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-17","reactions":{},"formalized":true,"formalizes":[{"title":"Paley graphs and Sárközy's theorem in function fields","identifier":"doi:10.1093/qmath/haac035","relationship":"adapts"}]}