Open Research Index

savarin/lean-malliavin

Ezzeri Esa

Palomar Registrypalomar/PALOMAR-2026-08-29-000016Aug 29, 2026math.PRscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-29-000016
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000016/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000016/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'