{"id":"palomar/PALOMAR-2026-09-07-000012","url":"https://github.com/GrgAakash/moh-p3-set-theoretic-complete-intersection/tree/abbdac729c91a6c7784a3dd15ff6828f2ce6e7fc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-07-000012-v2.json","repo":"https://github.com/GrgAakash/moh-p3-set-theoretic-complete-intersection","tags":["math.AC","math.AG","msc:13C40","msc:14M10","msc:13H05","msc:13P10","algebraic-geometry","commutative-algebra","lean","formalization"],"score":0,"title":"Moh's P3 curve is a set-theoretic complete intersection","trust":"high","domain":"math.AC","source":"palomar","authors":["Aakash Gurung"],"reviews":0,"subject":"math.AC","summary":"A Lean 4 formalization proving that the Moh curve parametrized by x=t^6+t^31, y=t^8, z=t^10 is cut out set-theoretically by two explicit equations over every characteristic-zero field. The development computes the polynomial and formal-power-series parametrization kernels, proves the radical equality for the two-generated witness ideal, and proves that the curve ideal has height two and arithmetic rank two, both globally and after completion. It also verifies the exact Hilbert-Burch presentation given by the manuscript's explicit four-by-three matrix.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Moh's P3 Curve Is a Global Set-Theoretic Complete Intersection","identifier":"","relationship":"formalizes"}]}