The sharp finite-field Nikodym exponent

Ting-Wei Chao, Zach Hunter, Cosmin Pohoata, Hung-Hsun Hans Yu, Shengtong Zhang

Palomar Registrypalomar/PALOMAR-2026-09-06-000002Sep 6, 2026math.COscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-06-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-06-000002/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-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'