Provenance and ownership

Attribution

ASTIS separates the textbook route, Mathlib facts, external proof references, ASTIS-owned Lean declarations, and generated exposition.

Organizers

The research and formalization team

Dake Bu · Ji Cheng · Atsushi Nitanda · Hau-San Wong · Qingfu Zhang

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.

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.

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 Hierarchical Automated
                  Theorem Proving System for Sampling Theory},
  author       = {Dake Bu and Ji Cheng and Atsushi Nitanda and
                  Hau-San Wong and Qingfu Zhang},
  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: 644be936998ef7714dbeb967a1a6df6d50670e71
Remote: https://github.com/DakeBU/Auto-Sampling-Theory-In-Sleep
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.