Delphi.science

savarin/lean-malliavin

Source: github.com/savarin/lean-malliavin/tree/29c57b3eba99625e8c7f…

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.

RepositoryJSON

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}'