Primary mathematical source
Sinho Chewi's Log-Concave Sampling determines the chapter route. ASTIS uses original summaries, exact source correspondence, and supplemental regularity details; it does not imply author endorsement.
Provenance and ownership
Attribution
ASTIS separates the textbook route, Mathlib facts, external proof references, ASTIS-owned Lean declarations, and generated exposition.
Project
Contributions and attribution
Project authorship is not yet finalized. Source authorship and software attribution below are independent of project membership.
Lean and Mathlib
Lean checks the local declarations. Mathlib supplies the measure, probability, analysis, convexity, kernel, and calculus APIs. A Mathlib theorem is labeled external until ASTIS owns the local declaration that consumes it.
External papers and repositories
Cited textbooks, papers, lean-stat-learning-theory, and Lean-Asymptotic-Statistical-Theory are audited references or port sources. Their licenses and theorem hypotheses remain controlling.
ATLAS v1 contributes a pinned 26-book external declaration index. It is limited to academic/research use under CC BY-NC 4.0; commercial use and ML model training, fine-tuning, distillation, evaluation, or development are prohibited; all 36,469 records remain external-reference until a local ASTIS theorem passes the current gate.
Design provenance
Comparisons with adjacent automation and formalization systems are centralized on the Related Systems page. This attribution page records ownership, mathematical sources, and software dependencies.
Citation
Cite ASTIS and Samplinglib
@misc{bu2026astis,
title = {Auto-Sampling-Theory-In-Sleep: A Substantive-Advance Automated
Theorem Proving System for Sampling Theory},
year = {2026},
howpublished = {GitHub repository and Samplinglib formalization website},
url = {https://github.com/DakeBU/Auto-Sampling-Theory-In-Sleep}
}Source state
- Git ref
main- Commit
0e31a3cda4122261f4c6fa35d0b75adeb6b23552- Remote
https://github.com/DakeBU/Automization-Sampling-Optimisation-Geometry-Lib- Published commit
- yes
- Public source links
- enabled
Source-link rule
By default every declaration links to the generated module anchor, so private or unpublished repositories cannot create public 404s. Set ASTIS_PUBLIC_SOURCE_LINKS=1 only after verifying that the remote is public; clean files at a remote-published commit then link to that exact SHA. Modified or untracked files always remain labeled “local preview source”. The generator never assumes that checkout content already exists on main.
Textbooks and formal upstreams
Additional Samplinglib library sources
Nicolas Boumal
An Introduction to Optimization on Smooth Manifolds supplies the Riemannian route.
Book site ↗Sinho Chewi
Lectures on Optimization (arXiv:2605.07006) supplies the public Optimisation formalization route.
arXiv PDF ↗Chewi · Niles-Weed · Rigollet
Statistical Optimal Transport supplies the OT source route. Villani, Santambrogio and Ambrosio–Gigli–Savaré provide targeted background for omitted details, not replacement source theorems.
Public textbook ↗Chen · Štefankovič · Vigoda
Spectral Independence and Local-to-Global Techniques for Optimal Mixing of Markov Chains, arXiv:2307.13826v4, supplies the Discrete Sampling spine. Levin–Peres (with Wilmer) and Duminil-Copin supply targeted mixing/model background; §12 proofs are recovered from cited originals, not silently assumed.
Pinned monograph ↗Optlib
Audited convex-analysis and algorithm theorem source.
Repository ↗CvxLean
Audited optimization-problem and transformation source.
Repository ↗Mathematical source lineage
Primary source ≠ supplement ≠ background reference.
A primary source controls source-facing statements. An official same-author supplement is additional source material. Background books are used to fill standard omitted details or cross-check conventions. Formal upstreams are reused only after compatibility is checked.
Sinho Chewi · Log-Concave Sampling
The source-facing theorem order and statement authority for the sampling textbook route.
main.pdf ↗Sinho Chewi · Supplement to Log-Concave Sampling
Official Chapter 2 material omitted from the book for space; treated as source, not ASTIS-added mathematics.
supp.pdf ↗Sinho Chewi · Lectures on Optimization
The public theorem-proof source and chapter spine for the Optimisation Library.
arXiv:2605.07006 ↗Rigorous stochastic-calculus cross-checks used by ASTIS
Used when Chewi sketches standard stochastic-calculus details and formalization requires the hidden measurability, stopping, completion, or martingale hypotheses to be made explicit.
Stochastic analysis and optimal-transport background recommended by Chewi
Chewi's bibliographical notes point readers to standard books when the main text omits routine or technical proofs. Samplinglib uses these as background/rigor references, never as silent replacements for the pinned Chewi theorem.
- Steele, Stochastic Calculus and Financial Applications
- Pavliotis, Stochastic Processes and Applications
- Le Gall, Brownian Motion, Martingales, and Stochastic Calculus
- Bakry-Gentil-Ledoux, Analysis and Geometry of Markov Diffusion Operators
- van Handel, Probability in High Dimension
- Villani, Topics in Optimal Transportation
- Ambrosio-Gigli-Savare, Gradient Flows in Metric Spaces and in the Space of Probability Measures
- Santambrogio, Optimal Transport for Applied Mathematicians
- Villani, Optimal Transport: Old and New
Concentration and functional-inequality background
Used to expand concentration, isoperimetry, and functional-inequality arguments around Chapter 2 when the source presentation is intentionally compact.
- Ledoux, The Concentration of Measure Phenomenon
- Boucheron-Lugosi-Massart, Concentration Inequalities
- Bakry-Gentil-Ledoux, Analysis and Geometry of Markov Diffusion Operators
- van Handel, Probability in High Dimension
- Vershynin, High-Dimensional Probability
Bubeck · Beck · Nesterov
Chewi explicitly states that the 2026 lecture notes are primarily based on these sources. They are attributed background and theorem cross-checks; the public formalization follows Chewi's arXiv notes.
- Sébastien Bubeck, Convex Optimization: Algorithms and Complexity (2015) — Named by Chewi as one of the principal sources underlying the lecture notes.
- Amir Beck, First-Order Methods in Optimization (2017) — Named by Chewi as one of the principal sources underlying the lecture notes; used for cross-checking and additional detail, but not as the public formalization spine.
- Yurii Nesterov, Lectures on Convex Optimization (2018) — Named by Chewi as one of the principal sources underlying the lecture notes.