Textbook
Log-Concave Sampling
Chewi's source-aligned textbook graph plus official supplement.
Verified Sampling, Optimisation, Geometry Theory in Lean
Samplinglib
Understand sampling, optimisation, and geometry through readable explanations, shared proof mechanisms, and exact Lean evidence. Start with an idea; follow its assumptions and proof at the depth you need.
Our mission in Math 2.0
Explore our nine contribution directions →Make verified mathematics easier to understand.
Build a living knowledge network and reusable Lean library. Use their proof structure to explain difficult ideas, improve learning, and open new research routes.
Research frontier
SampleWiki
Source-pinned frontier results and theorem-sized graph insertions.
Chapter scaffold
Riemannian Optimization
Boumal's eleven chapters on geometry and manifold algorithms.
Public arXiv formalization
Optimisation
Sinho Chewi's Lectures on Optimization with formal-upstream reuse.
Chapter scaffold
Statistical Optimal Transport
Chewi · Niles-Weed · Rigollet. Eight chapters and two appendices in the shared reader.
Finite-state source scaffold
Discrete Sampling
Ising / Glauber, hard-core and matroid sampling. Not continuous-state time discretization.
Method-family source scaffold
Markov Chain Monte Carlo
Fearnhead · Nemeth · Oates · Sherlock. Modern MCMC, shared kernels, scalable algorithms and estimation.
Current Progress
One collaboration dashboard for all seven routes.
SampleWiki Routedependency-first path to frontier results
Riemannian OptimizationBoumal source route
OptimisationSinho Chewi · arXiv:2605.07006
Statistical Optimal Transport Routetransport, geometry and statistics
Higher-Order Smoothness × Samplingfixed-oracle, cost-aware research
Discrete Sampling RouteIsing / Glauber and finite-state mixing
Markov Chain Monte Carlo RouteKernel design, scaling, general-state convergence and estimation
ASTIS Harness
One verification and reuse protocol for every route.
Each theorem-sized task is a Frontier Cell. Parallel workers may explore independently, but shared lower-level lemmas are searched/reused first, new shared foundations get one canonical shared cell, and only independently verified work enters the single stabilization lane.
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.
From proofs to verified mathematical structure
ASTIS turns source-backed mathematics into Lean-checked reusable graph memory.
Read the supporting proofs
Mathematical derivations with optional Lean and source details.