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 attribution
Authorship is not yet finalized
No provisional project author list is published. Mathematical source attribution is maintained separately below.
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.
OpenAI Math contributes Apache-2.0 manuscripts and proof artifacts pinned to its October 6, 2026 release. Comparator evidence and OAI.* declarations remain external references; they become neither blue ASTIS nodes nor solid local proof edges until an ASTIS-owned adapter or theorem passes local compilation and source-fidelity review. Open the seven-library intake map.
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 the workshop technical report
NeurIPS 2026 Workshop MATH-AI · OpenReview. The citation below identifies the published workshop paper, not a provisional list of library contributors.
@inproceedings{bu2026astis,
author = {Bu, Dake and Cheng, Ji and Zhou, Huanjian and Han, Andi and Chen, Zonghao and Wong, Hau-San and Zhang, Qingfu and Nitanda, Atsushi},
title = {An Automated Theorem Proving System and Visualized Lean Library for Sampling Theory, Optimisation and Geometry},
booktitle = {NeurIPS 2026 Workshop MATH-AI},
year = {2026},
url = {https://openreview.net/forum?id=UkKpNtVED2}
}Source state
- Git ref
main- Commit
ed709a7f320dfd6046df99572ffec13dd4d1392b- 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 complete Lean module in the generated site, including imports and context, 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.
Research-resource organization
Optlib informs the mathematical topic hierarchy; Optimization × AI Forum informs the categorized resource directory. Only bibliographic facts are indexed from the Forum; no site code, prose or styling is copied. Optlib retains its Apache-2.0 license and author notices. No affiliation or endorsement is implied.
Project license: Apache-2.0
Original Samplinglib material is licensed under Apache-2.0; external material retains its own terms. License, historical reuse and third-party boundaries.