Primary textbook
Log-Concave Sampling
Sinho Chewi's book, reconstructed section by section with beginner explanations, hidden analytic contracts, source correspondence, and Lean evidence.
12chapters
Verified sampling theory in Lean
Samplinglib
A readable formal library for sampling theory: Sinho Chewi's Log-Concave Sampling, a live SampleWiki frontier, and the shared Lean proof graph beneath both.
Live research frontier
SampleWiki
Current sampling results become source-pinned cases, then reviewed Lean targets and reusable proof-technique nodes in the same formal graph.
Livehourly source watch
Progressive disclosure
Three zoom levels, one proof.
Mathematics
Definitions, theorem statements, intuition, and proof route in natural language.
Proof graph
Shared lemmas and proof-technique nodes show what really carries the argument.
Lean
Exact declarations, hypotheses, dependencies, consumers, source lines, and tests.