active01
Dependency-first Chewi spine
Continue the shortest prerequisite route through the Chewi textbook graph toward useful SampleWiki results.
Samplinglib · Current Progress
Seven routes, one collaboration board.
SampleWiki, Riemannian Optimization, Optimisation, Statistical Optimal Transport, Discrete Sampling, and higher-order sampling advance in parallel on one page. Each theorem-sized task is a Frontier Cell; lower-level mathematics is shared only after a reuse/compatibility audit, so collaborators can move independently without rebuilding the same Lean foundation.
Dependency-first frontier route
SampleWiki Route
Immediate priority: extend the verified Chewi spine until useful frontier sampling results can enter the same theorem graph with exact source fidelity.
Route milestones
active02
Source fidelity + theorem insertion
Audit frontier statements against primary papers, then attach verified declarations to the existing theorem graph.
planned03
Proximal / LMC / ULD / MALA foundations
Prioritize reusable analytic roots that unlock multiple frontier cases rather than isolated terminal proofs.
planned04
Frontier result closure
Advance the highest-value reachable SampleWiki cells once their shared parents are stable.
Boumal route
Riemannian Optimization
Formalize Boumal while sharing only mathematically identical geometry foundations with the sampling route. Convention differences stay explicit in adapters.
Route milestones
scaffold01
Boumal source map
The eleven-chapter public route and source boundaries are established.
planned02
Shared geometry floor
Audit Mathlib and Samplinglib first; Chewi sampling §2.5 is the first explicit cross-route checkpoint.
planned03
Boumal Chapters 1–4
Definitions, embedded first-order geometry, and first-order Riemannian algorithms.
planned04
Boumal Chapters 5–11
Second-order geometry/algorithms, general and quotient manifolds, additional tools, and geodesic convexity.
Sinho Chewi · arXiv:2605.07006
Optimisation
Formalize Chewi's public optimization notes section by section, reusing Mathlib/Optlib/CvxLean and exposing exact shared convex/proximal/mirror foundations with sampling.
Route milestones
scaffold01
Chewi Lectures on Optimization source map
The public formalization spine follows arXiv:2605.07006: §§1–13 plus Appendix A.
planned02
Convexity, flow, descent, acceleration
Formalize §§1–5 while reusing compatible Mathlib/Optlib declarations.
planned03
Non-smooth, Frank-Wolfe, proximal, duality
Formalize §§6–9 and expose exact shared foundations with sampling when statements coincide.
planned04
Mirror, alternating, stochastic, interior-point
Formalize §§10–13 and audit sampling intersections around mirror/proximal/stochastic structure.
Chewi · Niles-Weed · Rigollet
Statistical Optimal Transport Route
Eight chapters and two appendices share the same reader, source-fidelity protocol and canonical Lean floor as the existing libraries.
Route milestones
scaffold01
Source map and shared entry points
8 chapters + A/B; exact page anchors. Audit convexity, probability and existing coupling code before introducing anything new.
planned02
Chapter 1: transport foundation
Couplings, Wasserstein distance, Brenier and duality. Reuse shared convex/marginal/compactness ingredients.
planned03
Parallel branches after Chapter 1
2–3 statistical estimation; 4 entropic transport; 5→6 flows and sampling; 7→8 metric geometry and barycenters.
planned04
Source omissions and transport review
Use Villani / Santambrogio / AGS for missing analytic details. Separate conceptual correspondence from certified Lean reuse.
Optimisation × Sampling research route
Higher-Order Smoothness × Sampling
Determine when additional potential smoothness yields a real sampling advantage at a fixed oracle and total computational cost. Existing high-order sampling literature is the starting point, not a novelty claim.
Route milestones
planned01
Regime and oracle matrix
Separate potential smoothness p, derivative access q, dynamical order k and discretization order r; fix metric, starts and dimension-dependent constants.
planned02
Shared Taylor and stochastic local error
Search existing Taylor, moment and coupling APIs; prove one useful local-error/invariant-target interface before a full rate.
planned03
Mixing plus discretization
Couple an audited local error with a compatible contraction theorem; count derivative evaluations and matrix/tensor work, not iterations alone.
parallel04
Lower bounds remain an independent lane
SampleWiki studies hard instances and information transcripts. Compare the two lanes only after oracle, class, metric and costs match.
Chen · Štefankovič · Vigoda
Discrete Sampling Route
Finite-state Ising/Glauber, hard-core and matroid sampling. Same shared graph and source/mirror gates; not continuous-sampling time discretization.
Route milestones
scaffold01
Pinned source and Ising entry
12 sections, 72 anchors; read Ising definitions early. Section 12 mixing proofs must be recovered from cited original papers.
planned02
Shared finite probability and kernel floor
Reuse PMF, measures, kernels and finite linear algebra; fix support, feasible pinnings, reversibility and clock before mixing.
planned03
Dirichlet / entropy / local-to-global
Pull §3 forward; prove finite dissipation adapters, uniform conditional-influence bounds and factorization with the exact normalization.
candidate04
Cross-domain conceptual mirrors
PI/chi-square, modified LSI/KL, finite transport geometry and conditional covariance. Independent source review never substitutes for a Lean transport certificate.
Fearnhead · Nemeth · Oates · Sherlock
Markov Chain Monte Carlo Route
General-state kernel construction, scalable MCMC and estimation. Shared with continuous and discrete sampling without identifying a method family with a target class.
Route milestones
planned01
Kernel → invariance → convergence
§§1.3,2.1 and Roberts–Rosenthal §§2–4; no SDE/RKHS bottleneck for finite MH or Gibbs.
planned02
Diffusions / geometry / estimation branch separately
ULA and MALA reuse shared analysis with exact clock/bias adapters; HMC and PDMP need augmented-state contracts.
scaffold03
Six primary chapters and ten extensions
Every extension has a parent chapter and its own pinned source. No theorem-completion credit.
candidate04
Conceptual bridges with independent review
Metropolis correction, weak limits, lifting, perturbation and block conditionals. Candidate labels never certify formal transport.
Shared Lean floor
Parallel above; canonical below.
Chewi sampling §2.5 ↔ Boumal
Riemannian manifolds, tangent-space/differential interfaces, gradients, metrics, and related analysis are candidates for one canonical shared foundation after convention compatibility is proved.
Chewi sampling §4.3 / Ch. 8 / Ch. 10 ↔ Chewi Optimisation
Convex analysis, proximal structure, mirror geometry, and stochastic-gradient primitives may be shared. Sampler kernels, invariant-law arguments, and route-specific source theorems remain separate.
Reuse → adapt → shared cell
Exact match → reuse. Near match → canonical core plus explicit adapter. Missing theorem needed by multiple routes → one shared Frontier Cell. Different theorem → keep separate.
ASTIS Harness · collaborative contract
One state machine, one shared Lean floor.
claimed→proved locally→independently verified→stabilized→merged
blocked→smaller child theorem→verified→re-entry
Search and classify
Search Samplinglib, Mathlib, active shared cells, and relevant formal upstreams. Record reuse, adapt, missing, or out_of_scope before adding a declaration.
One canonical shared cell
If two routes need the same missing lower-level theorem, record decision: new_canonical_shared, keep the route-local cell at claimed, and open/depend on one route: shared Frontier Cell. Parallel duplicate implementations are rejected by the protocol validator.
Single stabilization lane
Shared aggregators, root registries, duplicate API resolution, graph regeneration, and final root builds are serialized after independent verification.
Shared-foundation Frontier Cells
ASTIS-SHARED-canonical-fisher-transport-pairingproved locallyCanonical relative score paired with an optimal coupling
For a coupling gamma of finite-second-moment measures mu and nu, the pairing of gradient(logRatio mu pi)(x) with y-x is integrable whenever the existing smooth finite score domain holds. If gamma is quadratic-optimal, the absolute pairing integral is at most sqrt(information mu pi hscore) times wassersteinDistance mu nu toReal. Measurability, integrability and finite real cost identification are proved, not added as pairing premises.
ASTIS-SHARED-conditional-resampling-lawindependently verifiedRecover a joint law from a marginal and conditional distribution
For measurable spaces α and nonempty Standard-Borel β, a finite measure μ on α × β is recovered exactly by the composition-product of its first marginal and the regular conditional law of the second coordinate given the first.
ASTIS-SHARED-coordinate-heat-bathindependently verifiedOperational finite-coordinate heat-bath retention
For X : Fin(n+1) -> Type with measurable coordinates, finite mu including zero, and selected i with nonempty StandardBorel X i, define heatBath X mu i by inverse-map/comap conjugation of heatBathSnd through piFinSuccAbove then prodComm. It is Markov and invariant. For each retained j != i with MeasurableSingletonClass (X j), every input x has almost every output y satisfying y j = x j.
ASTIS-SHARED-coordinate-heat-bath-positive-fiberindependently verifiedActual coordinate heat-bath law on positive retained fibers
For dependent finite coordinates X, finite mu, selected i with Nonempty and StandardBorelSpace (X i), and MeasurableSingletonClass on the native retained product, heatBath X mu i x equals cond mu {y | retained_i y = retained_i x} whenever that fiber has nonzero mu mass.
ASTIS-SHARED-finite-kernel-mixtureindependently verifiedFixed finite convex mixtures preserve a common invariant law
For finite ι, fixed w : ι → ℝ≥0 with sum w = 1 and kernels κ i preserving the same arbitrary measure μ, construct the finite mixture and prove μ invariant. Markov components give a Markov mixture. The selected withDensity implementation requires s-finite component kernels, automatically supplied by Markovness; μ requires no finiteness or s-finiteness.
ASTIS-SHARED-gaussian-rgo-conditional-kernelindependently verifiedExplicit Gaussian RGO kernel and actual joint-law disintegration
For any probability law μ on finite-dimensional real inner-product Borel E and η>0, construct an actual measurable Markov kernel R with R(y)=μ.tilted(x↦−‖x−y‖²/(2η)) at every y, and prove that R disintegrates the swapped actual law of (X,X+sqrt(η)G), with independent X~μ and standard Gaussian G.
ASTIS-SHARED-heat-bath-snd-invarianceindependently verifiedSecond-coordinate heat-bath kernel preserves its finite joint law
For finite μ on α × β with measurable α and nonempty Standard-Borel β, construct heatBathSnd μ by retaining the first coordinate and drawing the second from condDistrib snd fst μ; show the kernel is Markov, has pointwise law dirac x.1 × condDistrib snd fst μ x.1, and leaves μ invariant. Exercise its finite powers through the existing invariant_pow interface.
ASTIS-SHARED-hessian-strong-convexityindependently verifiedA genuine second-derivative lower bound implies strong convexity
For a real normed space E, a C² real potential V and any real α, if α*‖v‖² ≤ D²V(x)[v,v] for every x,v, then StrongConvexOn univ α V. The second derivative is the derivative of the genuine first derivative supplied by C².
ASTIS-SHARED-isotropic-gaussian-densityindependently verifiedExplicit volume density of isotropic Gaussian noise
For every finite-dimensional real inner-product Borel space E and eta>0, the map of stdGaussian E by z -> sqrt(eta) z is volume.withDensity of ofReal((sqrt(2*pi*eta))^(-finrank R E) * exp(-norm(z)^2/(2*eta))). The natural-power inverse normalizer includes dimension zero. This is only the isotropic-noise density dependency; the augmentation identity is a separate next edge.
ASTIS-SHARED-kernel-invariant-transportindependently verifiedInvariant-kernel transport through a measurable equivalence
For arbitrary measurable spaces alpha and beta, arbitrary kernel kappa : Kernel alpha alpha and measure mu, and measurable equivalence e : alpha equiv beta, kappa.Invariant mu implies ((kappa.comap e.symm e.symm.measurable).map e).Invariant (mu.map e). No Markov, finite, s-finite, Standard Borel or nonempty hypotheses.
+ 50 additional registered cells.
Read the supporting proofs
Mathematical derivations with optional Lean and source details.