Live sampling frontier · source-to-Lean

SampleWiki

Turn source-pinned SampleWiki problems and proofs into reviewed Lean theorems and reusable ASTIS proof-technique nodes without confusing crawling, compilation, semantic review, and graph assimilation.

Open SampleWiki ↗

24pinned pages

34row-level cases

7tracked settings

6c4a330582f6case-tree fingerprint

Committed source state

The inventories below come from deterministic SampleWiki watchers. They are provenance metadata, not proof certificates. A changed result-row fingerprint reopens ASTIS triage and semantic review even when an older Lean declaration still compiles.

Truth boundary

Seven gates, not one “verified” badge

Only sourceReviewed or assimilated cases are eligible to feed the scientific ASTIS theorem graph.

`discovered`

The watcher found a page or result row.

`sourcePinned`

URL and cryptographic source fingerprints are fixed.

`normalized`

ASTIS writes an original mathematical restatement and assumption audit.

`leanTarget`

The exact Lean proposition and reusable leaf boundary are chosen.

`compiled`

The pinned Lean toolchain accepts the proof.

`sourceReviewed`

A reviewer checks theorem meaning against the pinned source.

`assimilated`

The theorem and proof-technique leaves enter the reusable ASTIS graph.

Live result frontier

One comparison-table row = one ASTIS source case

SampleWiki is organized by sampling assumptions and comparison tables. The case watcher therefore pins each result row separately: its setting, result class, algorithm/model, source review mark, source links, and row fingerprint. A source-pinned row is still not a Lean theorem until the later gates pass.

Case ID	Setting	Class	Algorithm / model	Upstream review mark	ASTIS stage	Row fingerprint
`ASTIS-SW-SETTING-CONVEX-BODY-MEMBERSHIP-BEST-UPPER-PROXIMAL-IN-AND-OUT-WITH-RESTART`	Convex body + membership oracle	best upper	Proximal / In-and-Out with restart	Cited preprint	`sourcePinned`	`4ed82a9e159f`
`ASTIS-SW-SETTING-CONVEX-BODY-MEMBERSHIP-LOWER-UNKNOWN-GENERAL-SAMPLING-LOWER-BOUND`	Convex body + membership oracle	lower unknown	General sampling lower bound	Unverified no primary source	`sourcePinned`	`c6e6860a0fdc`
`ASTIS-SW-SETTING-CONVEX-BODY-MEMBERSHIP-UPPER-R-NYI-PRESERVING-ANNEALING`	Convex body + membership oracle	upper	Rényi-preserving annealing	Cited preprint	`sourcePinned`	`2d7d9bcc05ad`
`ASTIS-SW-SETTING-CONVEX-BODY-MEMBERSHIP-UPPER-CONSTRAINED-PROXIMAL-SAMPLER`	Convex body + membership oracle	upper	Constrained proximal sampler	Checked published	`sourcePinned`	`f1655943a18e`
`ASTIS-SW-SETTING-FUNCTIONAL-INEQUALITY-SMOOTH-BEST-UPPER-IMPLEMENTED-PROXIMAL-SAMPLER`	Log-smooth + PI or LSI	best upper	Implemented proximal sampler	Checked monograph	`sourcePinned`	`c9e8f2e80e43`
`ASTIS-SW-SETTING-FUNCTIONAL-INEQUALITY-SMOOTH-LOWER-UNKNOWN-MATCHING-PI-LSI-ORACLE-LOWER-BOUND`	Log-smooth + PI or LSI	lower unknown	Matching PI/LSI oracle lower bound	Unverified no primary source	`sourcePinned`	`9b29d80a3e13`
`ASTIS-SW-SETTING-FUNCTIONAL-INEQUALITY-SMOOTH-UPPER-LMC`	Log-smooth + PI or LSI	upper	LMC	Checked monograph	`sourcePinned`	`9d98df6c5e84`
`ASTIS-SW-SETTING-FUNCTIONAL-INEQUALITY-SMOOTH-UPPER-LMC-R-NYI-INTERPOLATION`	Log-smooth + PI or LSI	upper	LMC Rényi interpolation	Checked monograph	`sourcePinned`	`0273c4725e5e`
`ASTIS-SW-SETTING-FUNCTIONAL-INEQUALITY-SMOOTH-UPPER-ULMC-WARM-START-CONSTRUCTION`	Log-smooth + PI or LSI	upper	ULMC warm-start construction	Checked monograph	`sourcePinned`	`24cf96a6b73a`
`ASTIS-SW-SETTING-HOLDER-SMOOTH-LOG-CONCAVE-BEST-UPPER-FORS-PROXIMAL-SAMPLER`	Weakly smooth log-concave	best upper	FORS + proximal sampler	Cited preprint	`sourcePinned`	`edb3cd2cfcac`
`ASTIS-SW-SETTING-HOLDER-SMOOTH-LOG-CONCAVE-LOWER-UNKNOWN-MATCHING-H-LDER-MODEL-LOWER-BOUND`	Weakly smooth log-concave	lower unknown	Matching Hölder-model lower bound	Unverified no primary source	`sourcePinned`	`26432c8ed091`
`ASTIS-SW-SETTING-HOLDER-SMOOTH-LOG-CONCAVE-UPPER-AVERAGED-LMC`	Weakly smooth log-concave	upper	Averaged LMC	Checked monograph	`sourcePinned`	`babd7760e808`
`ASTIS-SW-SETTING-HOLDER-SMOOTH-LOG-CONCAVE-UPPER-NONSMOOTH-MIRROR-LANGEVIN`	Weakly smooth log-concave	upper	Nonsmooth mirror-Langevin	Checked monograph	`sourcePinned`	`ba44eaedc763`
`ASTIS-SW-SETTING-LOG-CONCAVE-SMOOTH-BEST-UPPER-IMPLEMENTED-PROXIMAL-SAMPLER`	Log-concave + log-smooth	best upper	Implemented proximal sampler	Checked monograph	`sourcePinned`	`0c93b235281e`
`ASTIS-SW-SETTING-LOG-CONCAVE-SMOOTH-LOWER-UNKNOWN-MATCHING-FIRST-ORDER-LOWER-BOUND`	Log-concave + log-smooth	lower unknown	Matching first-order lower bound	Unverified no primary source	`sourcePinned`	`da4f4a11041c`
`ASTIS-SW-SETTING-LOG-CONCAVE-SMOOTH-UPPER-FORS-IMPLEMENTED-PROXIMAL-SAMPLER`	Log-concave + log-smooth	upper	FORS-implemented proximal sampler	Cited preprint	`sourcePinned`	`b280bbe6689e`
`ASTIS-SW-SETTING-LOG-CONCAVE-SMOOTH-UPPER-AVERAGED-LMC`	Log-concave + log-smooth	upper	Averaged LMC	Checked monograph	`sourcePinned`	`7a02639c1661`
`ASTIS-SW-SETTING-LOG-CONCAVE-SMOOTH-UPPER-IDEAL-PROXIMAL-CHAIN`	Log-concave + log-smooth	upper	Ideal proximal chain	Checked monograph	`sourcePinned`	`57687ebfab7f`
`ASTIS-SW-SETTING-NONLOGCONCAVE-FISHER-BEST-UPPER-EXACT-ULD-FORS`	Smooth non-log-concave + Fisher accuracy	best upper	Exact ULD / FORS	Checked preprint	`sourcePinned`	`979f9c367b59`
`ASTIS-SW-SETTING-NONLOGCONCAVE-FISHER-BEST-LOWER-GENERAL-FIRST-ORDER-FISHER-LOWER-BOUND`	Smooth non-log-concave + Fisher accuracy	best lower	General first-order Fisher lower bound	Checked published	`sourcePinned`	`f0b372fb2da1`
`ASTIS-SW-SETTING-NONLOGCONCAVE-FISHER-UPPER-LOWER-AVERAGED-LMC`	Smooth non-log-concave + Fisher accuracy	upper/lower	Averaged LMC	Checked monograph	`sourcePinned`	`e5f29efb15b8`
`ASTIS-SW-SETTING-NONLOGCONCAVE-FISHER-LOWER-ONE-DIMENSIONAL-FIRST-ORDER-FISHER-LOWER-BOUND`	Smooth non-log-concave + Fisher accuracy	lower	One-dimensional first-order Fisher lower bound	Checked published	`sourcePinned`	`c14844a53695`
`ASTIS-SW-SETTING-NONLOGCONCAVE-FISHER-LOWER-LARGE-INITIAL-GAP-QUERY-COMPLEXITY`	Smooth non-log-concave + Fisher accuracy	lower	Large-initial-gap query complexity	Checked published	`sourcePinned`	`12e7c0835d5d`
`ASTIS-SW-SETTING-STOCHASTIC-FINITE-SUM-BEST-UPPER-HIGH-ACCURACY-STOCHASTIC-GRADIENT-SAMPLER`	Stochastic and finite-sum oracles	best upper	High-accuracy stochastic-gradient sampler	Checked published	`sourcePinned`	`a409105a2ae0`
`ASTIS-SW-SETTING-STOCHASTIC-FINITE-SUM-BEST-LOWER-BOUNDED-VARIANCE-STOCHASTIC-GRADIENT-LOWER-BOUND`	Stochastic and finite-sum oracles	best lower	Bounded-variance stochastic-gradient lower bound	Checked published	`sourcePinned`	`bacb310edd2d`
`ASTIS-SW-SETTING-STOCHASTIC-FINITE-SUM-UPPER-VARIANCE-REDUCED-HIGH-ACCURACY-SAMPLER`	Stochastic and finite-sum oracles	upper	Variance-reduced high-accuracy sampler	Checked published	`sourcePinned`	`8a30ba8b7629`
`ASTIS-SW-SETTING-STOCHASTIC-FINITE-SUM-UPPER-FINITE-SUM-RM-ULMC`	Stochastic and finite-sum oracles	upper	Finite-sum RM-ULMC	Checked monograph	`sourcePinned`	`40e4d538a222`
`ASTIS-SW-SETTING-STOCHASTIC-FINITE-SUM-LOWER-FINITE-SUM-ZEROTH-ORDER-LOWER-BOUND`	Stochastic and finite-sum oracles	lower	Finite-sum zeroth-order lower bound	Checked monograph	`sourcePinned`	`5e45cd49aab8`
`ASTIS-SW-SETTING-STRONGLY-LOG-CONCAVE-SMOOTH-BEST-UPPER-EXACT-ULD-FORS`	Strongly log-concave + log-smooth	best upper	Exact ULD / FORS	Cited preprint	`sourcePinned`	`2de79774ed38`
`ASTIS-SW-SETTING-STRONGLY-LOG-CONCAVE-SMOOTH-BEST-LOWER-GENERAL-FIRST-ORDER-ORACLE-LOWER-BOUND`	Strongly log-concave + log-smooth	best lower	General first-order oracle lower bound	Checked published	`sourcePinned`	`f6b7a4718591`
`ASTIS-SW-SETTING-STRONGLY-LOG-CONCAVE-SMOOTH-UPPER-MALA`	Strongly log-concave + log-smooth	upper	MALA	Checked monograph	`sourcePinned`	`3b4c095bd509`
`ASTIS-SW-SETTING-STRONGLY-LOG-CONCAVE-SMOOTH-UPPER-RANDOMIZED-MIDPOINT-ULMC`	Strongly log-concave + log-smooth	upper	Randomized-midpoint ULMC	Checked monograph	`sourcePinned`	`057445807a89`
`ASTIS-SW-SETTING-STRONGLY-LOG-CONCAVE-SMOOTH-UPPER-BLOCK-KRYLOV-GAUSSIAN-SAMPLER`	Strongly log-concave + log-smooth	upper	Block-Krylov Gaussian sampler	Checked monograph	`sourcePinned`	`3c28169d5e86`
`ASTIS-SW-SETTING-STRONGLY-LOG-CONCAVE-SMOOTH-LOWER-MALA-LOWER-BOUND`	Strongly log-concave + log-smooth	lower	MALA lower bound	Checked monograph	`sourcePinned`	`032fb49df877`

Source graph

Same-origin pages behind the cases

The crawler separately records bounded page structure and cryptographic fingerprints. This lets ASTIS distinguish a navigation/prose edit from a changed mathematical row instead of treating the whole website as one blob.

Source page	Headings	Text fingerprint
samplewiki	samplewiki · News · Choose the assumptions first. · Convex body + membership oracle	`89c6184c0f2c`
News · samplewiki	News	`9fe21b9a40cf`
Review marks · samplewiki	Review and publication are different facts. · Review state · Source state · Comparison rule	`5d5fe3b5f3bd`
Page · samplewiki	Convex body + membership oracle · Comparison table · Scope · Lower bounds	`60bfdaf0455c`
Discussion · samplewiki	—	`f5f865c7aafa`
Page history · samplewiki	History: Convex body + membership oracle	`3a2429cee89e`
Page · samplewiki	Log-smooth + PI or LSI · Comparison table · Scope · Lower bounds	`65e0530f2343`
Discussion · samplewiki	—	`f5f865c7aafa`
Page history · samplewiki	History: Log-smooth + PI or LSI	`04da59fc12ee`
Page · samplewiki	Weakly smooth log-concave · Comparison table · Scope · Lower bounds	`ab9b6ce461c5`
Discussion · samplewiki	—	`f5f865c7aafa`
Page history · samplewiki	History: Weakly smooth log-concave	`d18987b5aa28`
Page · samplewiki	Log-concave + log-smooth · Comparison table · Scope · Lower bounds	`5f4c4850ffd3`
Discussion · samplewiki	—	`f5f865c7aafa`
Page history · samplewiki	History: Log-concave + log-smooth	`3badcaf586b8`
Page · samplewiki	Smooth non-log-concave + Fisher accuracy · Comparison table · Scope	`ef30d1d8fd5f`
Discussion · samplewiki	—	`f5f865c7aafa`
Page history · samplewiki	History: Smooth non-log-concave + Fisher accuracy	`48fad0617e35`
Page · samplewiki	Stochastic and finite-sum oracles · Comparison table · Scope · Main separation	`17a8271bdb05`
Discussion · samplewiki	—	`f5f865c7aafa`
Page history · samplewiki	History: Stochastic and finite-sum oracles	`1cdb69d27fd8`
Page · samplewiki	Strongly log-concave + log-smooth · Comparison table · Scope · Reading the frontier	`a9681d7b3492`
Discussion · samplewiki	—	`f5f865c7aafa`
Page history · samplewiki	History: Strongly log-concave + log-smooth	`6697f97095bb`

How one case becomes Lean

Pin the exact comparison-table result row and its source references.
Write an original ASTIS mathematical restatement.
Audit visible and hidden assumptions.
Search Mathlib and Samplinglib before adding a leaf.
Formalize missing reusable leaves bottom-up.
Compile a thin source-facing assembly theorem.
Review semantic fidelity against the pinned source.
Assimilate theorem and proof-technique nodes into the shared DAG.

Parallel-lane rule

Prefer cases whose prerequisites already exist on main; reuse Chapter 1.1 and Chapter 1.2–1.3 roots after they merge instead of creating SampleWiki-specific duplicates.

The Example Cases lane may therefore keep advancing on source cases that depend only on stable main declarations while Chapter 1.1 and Chapter 1.2–1.3 continue independently.

What counts as progress?

A new source row is discovery progress. A source-pinned ASTIS restatement is specification progress. A compiled Lean theorem is formal proof progress. Semantic source review is fidelity progress. Only assimilation makes the theorem and its proof technique part of the reusable Samplinglib scientific graph. These states remain visible separately.