{"id":"palomar/PALOMAR-2026-10-09-000014","url":"https://github.com/amelieloher/hoermander-rothschild-stein/tree/d1462014b4ca69cf04b250582ea45021aa07b546","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-09-000014-v1.json","repo":"https://github.com/amelieloher/hoermander-rothschild-stein","tags":["math.AP","math.CA","math.DG","msc:35H10","msc:35H20","msc:43A80","msc:53C17","msc:22E25","hypoellipticity","pde"],"score":0,"title":"Hörmander's hypoellipticity theorem and the Rothschild–Stein theory","trust":"high","domain":"math.AP","source":"palomar","authors":["Scott Armstrong","Amélie Loher"],"reviews":0,"subject":"math.AP","summary":"A Lean 4 / Mathlib formalization of the regularity theory of Hörmander operators: second-order operators built from smooth vector fields X_1, ..., X_q (and possibly a drift X_0) whose iterated commutators span the tangent space at every point. It proves Hörmander's 1967 theorem that such operators are hypoelliptic: every locally integrable weak solution of X_0 u + sum X_i^2 u + c u = g with smooth data is smooth. It then develops the Rothschild–Stein theory (Acta Math. 1976), following Bramanti and Brandolini's \"Hörmander Operators\" (2023): lifting and approximation of the fields by the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-09","reactions":{},"formalized":true,"formalizes":[{"title":"Hypoelliptic second order differential equations","identifier":"","relationship":"formalizes"},{"title":"Hypoelliptic differential operators and nilpotent groups","identifier":"","relationship":"formalizes"},{"title":"Hörmander Operators","identifier":"","relationship":"formalizes"},{"title":"Balls and metrics defined by vector fields I: Basic properties","identifier":"","relationship":"formalizes"}]}