Move a Mathematical Result into Verified Memory
Contribute a focused correction, reusable Lean leaf, textbook reconstruction, proof-route packet, diagram, or teaching improvement without blurring source mathematics, local proof evidence, and route completion.
One result, explicit ownership, independent review
flowchart LR
A["1 · Discuss<br/>fix the mathematical scope"] --> B["2 · Locate ownership<br/>search Samplinglib and Mathlib"]
B --> C{"Contribution type"}
C -->|Reusable leaf| D["Subject module<br/>TechnicalLemmas"]
C -->|Book or paper result| E["Consumer theorem<br/>source correspondence"]
C -->|Open work| F["Typed ASTIS packet<br/>honest route status"]
D --> G["3 · Verify<br/>Lean build · ASTIS gate · site check"]
E --> G
F --> G
G --> H{"Independent review"}
H -->|accepted certificate| I["4 · Integrate<br/>Samplinglib formal memory"]
H -->|exact blocker| J["Return to owning layer"]
J --> B
classDef source fill:#172033,stroke:#172033,color:#fff,stroke-width:2px;
classDef leaf fill:#DCEBFF,stroke:#155EEF,color:#172033,stroke-width:1.5px;
classDef route fill:#FFF3D6,stroke:#B54708,color:#172033,stroke-width:1.5px;
classDef gate fill:#DCFAE6,stroke:#087443,color:#172033,stroke-width:1.5px;
classDef review fill:#ECE6FF,stroke:#6938EF,color:#172033,stroke-width:1.5px;
class A,B source;
class C,F,E route;
class D,I leaf;
class G gate;
class H,J review;
Fix the scope before a large development
Focused corrections, documentation repairs, and narrow API improvements can remain small. Open an issue before adding a theorem route, module or namespace, changing mathematical assumptions, porting a large external development, or changing the ASTIS gate.
Focused change
Keep the pull request narrow and name the declaration or page being corrected.
New route or boundary
State the result, exact source, owner module, dependencies, and whether it is a reusable leaf or a book/paper consumer.
Search first, then work in the owning layer
Search the declaration catalog, implementation map, local source, and Mathlib before creating an API. A nearby statement is reusable only when its hypotheses and semantics genuinely match.
| Contribution | Canonical owner | Admission rule |
|---|---|---|
| Reusable mathematical leaf | TechnicalLemmas/ subject module | Complete local proof; Registry only when selected for shared memory |
| Textbook or paper result | Consumer theorem plus exact source correspondence | Source statement, assumptions, constants, and proof boundary preserved |
| Open proof work | Typed ASTIS packet or paper-contribution memory | Remains Partial, Planned, Blocked, or External; never promoted by prose |
| Teaching or roadmap content | website/content/ | May reference only real declarations; route and local status stay separate |
| Diagram | website/diagrams/*.mmd | Editable source, real modules/declarations, checked generated rendering |
Two independent reports are mandatory: Local declaration status records what this checkout proves; Mathematical route/paper-reproduction status records how far the source theorem route has actually been reconstructed.
Reuse before extension. Prefer an existing Samplinglib or Mathlib declaration when it is an exact fit.
Complete proof boundary. Do not use sorry, admit, hidden axioms, constants, postulates, or fake trivial closure.
Preserve provenance. Keep original copyright and author notices for adapted code and record the exact source and substantive changes.
Run the library, harness, and website gates
Use the Lean and Mathlib revisions pinned by this checkout. From the repository root:
lake exe cache get
LEAN_NUM_THREADS=$(nproc) lake build
python3 tools/astis.py check
python3 tools/astis.py harness-test
python3 website/scripts/lean_gate.py
python3 website/scripts/build_site.py
python3 website/scripts/check_site.py- The whole Lean build succeeds.
- No forbidden proof placeholder or fake closure was introduced.
- Imports preserve subject ownership and avoid cycles.
- Sources, assumptions, constants, and endpoints are exact.
- Local proof status and route status are reported independently.
- New reusable leaves have focused evidence and warranted Registry metadata.
- Website metadata names only declarations in this checkout.
- Generated
_site/output remains uncommitted.
This build currently records 393 compiled Registry leaves. That count is a consistency baseline, not a claim that the Log-Concave Sampling route is complete.
Make the mathematical and formal evidence reviewable
Use the repository pull request template. Record the result and source anchor, owning module, API decisions, exact commands run, adapted-code provenance, both status layers, and every remaining obligation.
Reviewer checks
- source fidelity and hidden hypotheses;
- statement or constant drift;
- module ownership and duplicate APIs;
- proof completeness and current gate evidence;
- honest remaining mathematical frontier.
Credit
Accepted contributions are credited in Git history and relevant source-file author headers. Co-written commits should include one Co-authored-by trailer per additional author.
Co-authored-by: Full Name <email@example.com>Acceptance principle
Discussion and implementation can remain flexible, but admission to Samplinglib requires explicit mathematical ownership, source provenance, current Lean evidence, and an independent reviewer decision.