{"id":"palomar/PALOMAR-2026-09-06-000002","url":"https://github.com/ShengtongZhang-alt/Nikodym/tree/0cd3550000630f4653fac67db43c2d264a0ca426","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-06-000002-v1.json","repo":"https://github.com/ShengtongZhang-alt/Nikodym","tags":["math.CO","math.AG","msc:05B25","msc:11T06","msc:13D40","msc:14G15","finite-fields","combinatorics","lean-formalization"],"score":0,"title":"The sharp finite-field Nikodym exponent","trust":"high","domain":"math.CO","source":"palomar","authors":["Ting-Wei Chao","Zach Hunter","Cosmin Pohoata","Hung-Hsun Hans Yu","Shengtong Zhang"],"reviews":0,"subject":"math.CO","summary":"A complete Lean 4 / Mathlib formalization of the sharp power saving in the finite-field Nikodym problem. A set N in F_q^d is a Nikodym set if through every point x there is a line all of whose points other than x lie in N. Lower bound: for every finite field F_q, every d >= 2 and every Nikodym set N in F_q^d, |N| >= q^d - (8 d^2 + 1) q^(d - 2^(1-d)); the proof goes through a carrier theorem for integral projective varieties containing many affine lines with private points, proved by finite-grid Hermite interpolation, Hilbert-function estimates (normalized monotonicity and a degree upper…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-06","reactions":{},"formalized":true,"formalizes":[{"title":"Nikodym sets: a power saving from finite-grid interpolation","identifier":"docs/Nikodym_sharp_power_saving.tex (this repository, at the submitted commit)","relationship":"formalizes"},{"title":"A prime-uniform construction of small finite-field Nikodym sets","identifier":"docs/nikodym_construction.tex (this repository, at the submitted commit)","relationship":"formalizes"}]}