{"id":"palomar/PALOMAR-2026-08-31-000018","url":"https://github.com/savarin/lean-malliavin/tree/a1a6ccc6eedbdf15fc3aebf9146d1fddfa0c8272","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000018-v1.json","repo":"https://github.com/savarin/lean-malliavin","tags":["math.PR","math.FA","msc:60H07","msc:46E35","probability","malliavin-calculus","lean-formalization","gaussian-analysis"],"score":0,"title":"lean-malliavin","trust":"high","domain":"math.PR","source":"palomar","authors":["Ezzeri Esa"],"reviews":0,"subject":"math.PR","summary":"Malliavin calculus on abstract Gaussian Banach spaces, formalized in Lean 4 against Mathlib. The repository contains two Comparator configurations: one registered (core, via comparator.json, pinned at commit 29c57b3) and one pending (Clark--Ocone, via comparator-clark-ocone.json). The proof library (52 files) builds from Cameron--Martin quasi-invariance through the Wiener chaos decomposition and Itô isometry to the full representation formula.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"The Malliavin Calculus and Related Topics","identifier":"10.1007/3-540-28329-3","relationship":"adapts"},{"title":"The Malliavin Calculus and Related Topics","identifier":"10.1007/3-540-28329-3","relationship":"adapts"}]}