Design context
Related Systems
ASTIS combines long-horizon research control, Lean formalization, and a sampling-theory memory library. This is the sole website page that compares those design choices with adjacent systems.
Comparison boundary
What is reused, and what remains ASTIS-specific
| System | What informs ASTIS | ASTIS boundary |
|---|---|---|
| Learning Beyond Gradients ↗ | Role-separated iteration, durable trial memory, summaries, and rejected-route records. | ASTIS maps these ideas to upper planning, middle formalization, lower Lean work, and independent proof review; source correspondence and the compiler gate remain authoritative. |
| EoH ↗ | Population initialization, variation, selection, and archive pressure for competing routes. | Population search is allowed only for fixed Lean-checkable targets in exploratoryProof; faithfulPaper cannot mutate the source theorem, assumptions, or constants. |
| ARIS ↗ | Long-running research loops, plain-file handoffs, and separate reviewer passes. | ASTIS specializes the loop for Lean proof states, exact source anchors, analytic obligations, and reusable sampling-theory memory. |
| LeanMarathon ↗ | Blueprint-driven target selection, dynamic proof-DAG leaves, bounded workers, and deterministic gates. | ASTIS keeps a local source-backed harness and a separate Samplinglib memory layer instead of requiring a GitHub/PR/Slurm execution substrate. |
| MathCode ↗ | Lean diagnostics, theorem reuse, and explicit subgoal planning. | Diagnostics and retrieval remain advisory; only ASTIS-owned source correspondence, local compilation, tests, and reviewer evidence can accept a result. |
| Sho Sonoda / Lean-Ridgelet ↗ | Blueprint-style organization and an implementation map connecting mathematics to Lean declarations. | Samplinglib uses an independently implemented generator, a full textbook route, dual status, hidden-condition packets, and sampling/SDE-specific theorem DAGs. |
| StatsMLlib ↗ | Subject-owned Lean modules, reuse-first development, complete proofs, source attribution, and staged contribution review. | Samplinglib adds textbook-route correspondence, dual local/route status, typed ASTIS packets, and reviewer-controlled admission to formal memory. |
Interpretation
These links record design provenance. They do not imply code identity, theorem equivalence, endorsement, or local Lean proof ownership. Mathematical sources and software dependencies are documented separately under Attribution.