Design provenance and license boundary

Attribution

This site's organization is inspired by Sho Sonoda's Lean-Ridgelet Blueprint, especially its readable implementation map from mathematics to Lean.

Lean-Ridgelet inspiration

Lean-Ridgelet is a Lean formalization project by Sho Sonoda. Its Blueprint website demonstrates how publication-order mathematical exposition can link to verified declarations.

The upstream repository license was checked before implementation and is Apache License 2.0. ABRL uses an independently written Python generator, HTML structure, CSS, JavaScript, Mermaid diagrams, and prose. No Lean-Ridgelet source file, template, stylesheet, or configuration file is copied into this repository.

This attribution records inspiration only. It does not imply that Sho Sonoda participated in, reviewed, endorsed, or maintains Auto-Bandit-RL-Proof-In-Sleep.

StatsMLlib community inspiration

StatsMLlib and its public repository demonstrate an effective community-facing organization around a book map, selected theorems, contributor credit, installation, and a visible contribution guide.

StatsMLlib is Apache-2.0 licensed. ABRL independently implements its three-purpose learning, browsing, and contribution interface, its lemma-packet schema, governance documents, generator, HTML, CSS, JavaScript, and diagrams. No StatsMLlib template, stylesheet, prose, or source file is copied here.

This reference records organizational inspiration only. It does not imply that StatsMLlib, Lean-MoDS, its organizers, or its contributors participate in, endorse, review, or maintain ABRL.

Mathematical and software sources

The repository's full literature, Mathlib, LML, automation, and proof-system attribution ledger is maintained in docs/attribution.md and NOTICE.md.

Theorem cards summarize external results for retrieval. They do not transfer authorship and do not become local proof certificates until an import or local proof compiles.