{"id":"palomar/PALOMAR-2026-09-22-000003","url":"https://github.com/scottnarmstrong/CaffarelliKohnNirenberg/tree/58a9ffe548ea64319ac8cba098634340ee6270cb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-22-000003-v1.json","repo":"https://github.com/scottnarmstrong/CaffarelliKohnNirenberg","tags":["math.AP","msc:35Q30","msc:35B65","msc:76D05","msc:76D03","msc:35D30","pde","navier-stokes","regularity-theory","lean"],"score":0,"title":"CaffarelliKohnNirenberg","trust":"high","domain":"math.AP","source":"palomar","authors":["Scott Armstrong","Vlad Vicol"],"reviews":0,"subject":"math.AP","summary":"A Lean 4 / Mathlib formalization of the Caffarelli-Kohn-Nirenberg partial regularity theory for suitable weak solutions of the three-dimensional incompressible Navier-Stokes equations with forcing in L^q, q > 5/2: the L^3 epsilon-regularity theorem (Theorem A), the gradient epsilon-regularity criterion (Theorem B) and the vanishing of the one-dimensional parabolic Hausdorff measure of the singular set (Theorem C). The three theorems are proved using only the standard axioms, restated together in a Mathlib-only comparator challenge and proved from the library theorems. The manuscript being…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-22","reactions":{},"formalized":true,"formalizes":[{"title":"The Caffarelli--Kohn--Nirenberg partial regularity theorem: a self-contained proof written for formalization","identifier":"paper/ckn.tex","relationship":"formalizes"}]}