{"id":"palomar/PALOMAR-2026-08-29-000016","url":"https://github.com/savarin/lean-malliavin/tree/29c57b3eba99625e8c7f6b2eaccea7fb1c6cc5f7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000016-v1.json","repo":"https://github.com/savarin/lean-malliavin","tags":["math.PR","math.FA","msc:60H07","msc:46E35","malliavin-calculus","gaussian-analysis","lean-formalization","probability"],"score":0,"title":"savarin/lean-malliavin","trust":"high","domain":"math.PR","source":"palomar","authors":["Ezzeri Esa"],"reviews":0,"subject":"math.PR","summary":"Gaussian integration by parts and closability of the Malliavin derivative on an abstract Gaussian Banach space. Two compared theorems, zero definition holes. Challenge.lean (225 lines) states both results using only Mathlib definitions; Solution.lean bridges via definitional equality to the extracted Malliavin proof library.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true,"formalizes":[{"title":"The Malliavin Calculus and Related Topics","identifier":"10.1007/3-540-28329-3","relationship":"adapts"}]}