{"id":"palomar/PALOMAR-2026-08-30-000001","url":"https://github.com/BochaoKong/nullstellensatz/tree/029697242294aea7989bf5d391199696a43490df","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-30-000001-v1.json","repo":"https://github.com/BochaoKong/nullstellensatz","tags":["math.CV","math.AG","msc:32A10","msc:32B05","msc:32C25","msc:13E05","several-complex-variables","nullstellensatz","lean-formalization","analytic-geometry"],"score":0,"title":"BochaoKong/nullstellensatz","trust":"high","domain":"math.CV","source":"palomar","authors":["BochaoKong"],"reviews":0,"subject":"math.CV","summary":"A Lean 4 formalization of Rückert's Noetherianity theorem for local holomorphic-germ rings, algebraic and genuinely geometric finite projection for analytic hypersurface germs, the holomorphic constant-rank normal form, and Rückert's local analytic Nullstellensatz in finite-family and arbitrary-ideal radical forms.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-30","reactions":{},"formalized":true,"formalizes":[{"title":"Analytic Functions of Several Complex Variables","identifier":"https://doi.org/10.1090/chel/368","relationship":"formalizes"},{"title":"Introduction to Complex Analytic Geometry","identifier":"https://doi.org/10.1007/978-3-0348-7617-9","relationship":"formalizes"}]}