{"id":"palomar/PALOMAR-2026-09-05-000007","url":"https://github.com/itpplasma/stafford38-formal/tree/0bb3aa929b931bf5d82d90f62d7508d3ae1dccc1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-05-000007-v3.json","repo":"https://github.com/itpplasma/stafford38-formal","tags":["math.RA","msc:16S32","weyl-algebra","lean-formalization","ring-theory"],"score":0,"title":"Stafford 3.8","trust":"high","domain":"math.RA","source":"palomar","authors":["Christopher Albert"],"reviews":0,"subject":"math.RA","summary":"Lean formalization of Stafford's Conjecture 3.8 for every characteristic-zero field and every Weyl-algebra rank, proving that each nonzero d admits F, R, and S with 1 = d*R + F*d*S. The development also proves an exact Bernstein-degree fixed-source strengthening and derived localization, adjoint, and evolutionary results.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-04","reactions":{},"formalized":true}