Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
Sampling research

SampleWiki

New results, open questions and their proofs. Read the mathematics; open the checked Lean when you need it.

Formalization progress

Browse sampling regimes

Start with the target assumptions, oracle and accuracy notion. Compare results and open questions in that setting.

Convex body + membership oracle4 mathematical cases · 0 primary-source theorem audits · 1 open frontierLog-smooth + PI or LSI5 mathematical cases · 1 primary-source theorem audits · 1 open frontierWeakly smooth log-concave4 mathematical cases · 2 primary-source theorem audits · 1 open frontierLog-concave + log-smooth5 mathematical cases · 3 primary-source theorem audits · 1 open frontierSmooth non-log-concave + Fisher accuracy5 mathematical cases · 2 primary-source theorem auditsStochastic and finite-sum oracles5 mathematical cases · 0 primary-source theorem auditsStrongly log-concave + log-smooth6 mathematical cases · 1 primary-source theorem audits

Research resources: guides, formal libraries and papers

A textbook-linked worked example
Textbook-linked case study

Ideal proximal chain

Theorem statement
\[\operatorname{KL}(\mu_n^X\Vert\pi^X)\le \frac{W_2^2(\mu_0^X,\pi^X)}{nh}\]
Open theorem, proof route, and Lean boundary →

Selected research projects

Read a paper or case study, its proof route and the pieces verified so far.

Verified building blocks are not completed paper proofs.

How the warm start and high-accuracy sampler fit together →

Open mathematical questions

These are open in the literature, not merely missing Lean proofs.

Pinned external proof memory

OpenAI Math extension shelf

8 audited upstream routes are placed beside this library's real chapters or named Samplinglib extensions. External verification is shown separately from ASTIS compilation.

Open this library's map See all seven