Explain or connect
Improve a teaching note, add a literature pointer, identify a missing assumption, or connect an existing declaration to a textbook theorem.
Contribute to BanditRLlib
Bring one theorem. Leave a reusable Lean lemma.
BanditRLlib welcomes sourced mathematics from bandits, reinforcement learning, probability, optimization, statistics, and adjacent fields. Every proposal enters the existing ABRL hierarchy, keeping provenance, meaning, Lean text, dependencies, obligations, and verification status together.
Four steps to a reviewed contribution
- Source the mathematics.Name the paper, book, formal proof gap, or original result and state every assumption.
- Open a proposal.Agree on the target statement, namespace, module, and dependencies before a large implementation.
- Compile and document.Submit Lean code, tests, plain-English meaning, mathematical notation, and proof correspondence.
- Pass review and integration.Only the full project gate and maintainer review can mark the declaration integrated and compiled.
Three useful contribution sizes
Propose a lemma packet
Supply a sourced mathematical statement, LaTeX, a Lean draft or signature, expected imports, and dependencies. A draft is visibly marked proposed.
Submit a checked formalization
Contribute a compiling Lean implementation with tests and teaching prose. Maintainers still review API placement, assumptions, attribution, and integration.
How a lemma joins the library
A GitHub issue is enough to begin. Large formalizations should agree on scope and module ownership before substantial proof work. No proposal is displayed as compiled merely because it contains Lean-looking text.
flowchart LR
Proposal["Researcher proposal<br/>theorem + assumptions + source"] --> Packet["Contribution packet<br/>schema 1.1"]
Packet --> Middle["ABRL middle layer<br/>route and dependency review"]
Middle --> Lower["ABRL lower layer<br/>Lean implementation"]
Lower --> Compiler["Lean 4 compilation"]
Compiler --> Review["Statement fence + reviewer + full gate"]
Review -->|changes requested| Proposal
Review -->|accepted| Library["BanditRLlib on main"]
Library --> Credit["Contributor registry and release notes"]
PlannedProposed — sourced mathematics and a review packet exist.
PartialIn review — statement, assumptions, namespace, or proof is being checked.
CompiledLean checked — the submitted snippet compiles in the declared environment.
IntegratedIntegrated — reviewer-approved, merged into BanditRLlib on
main, and included in a verified snapshot.A stable contract for the future compiler
The community unit is a versioned JSON lemma packet. Live Formalization exports it today, including BanditRLlib reuse, Mathlib/LML candidates, semantic status, compiler status, and unresolved obligations. The packet becomes an ABRL task rather than a second proof system.
Required evidence
- stable contribution ID and mathematical domain;
- source paper, book, or original-result provenance;
- plain-English and LaTeX statements;
- Lean imports, declaration text, and named dependencies;
- verification status and compiler evidence;
- contributor identity, preferred credit, and license agreement.
{
"schema_version": "1.1",
"id": "domain-short-lemma-name",
"status": "proposed",
"mathematics": { "plain": "...", "latex": "..." },
"lean": { "imports": ["BanditRLProof"], "code": "...", "banditrl_reused": [] },
"provenance": { "source": "DOI, arXiv, book, or original" },
"contributor": { "name": "...", "credit": "..." },
"unresolved_proof_obligations": ["semantic review"]
}Trust boundary. GitHub Pages does not execute untrusted Lean code or call a model API. Local verified mode uses a loopback-only server; only semantic review, maintainer approval, and a passed full gate can move a proposal to BanditRLlib's integrated status.
Repository-enforced publication protocol
Collaborators and their Codex agents follow the same contract
Before substantial work, read AGENTS.md, CONTRIBUTING.md, docs/contributor-codex-contract.md, docs/theorem-publication-protocol.md, and the substantive-advance / semantic-roundtrip skills. The thin reusable bootstrap is .agents/prompts/collaborator-contribution.md.
Reuse before new Lean
Search BanditRLlib, Mathlib, LML and compatible upstreams. New shared leaves name real consumers; wrapper-only duplication is rejected by the contribution contract.
Encoder–denoiser source review
Source-facing claims require a formalizer, a distinct source-blind decoder, and a distinct anti-anchored source reviewer. Compilation alone never certifies source fidelity.
Reader publication
Keep source statement, natural-language formula proof, hidden assumptions, source-vs-Lean deltas, folded Lean, actual dependencies, and the remaining boundary together.
Three graph views
Every substantive delta classifies Lean Graph, Overview/route progress, and Functor Hypergraph. Formal structure is solid; source/planned/semantic/conceptual overlays stay dashed.
No silent website drift. Teaching route, BanditRLwiki, result/roadmap status, graph views and contributor/provenance surfaces are either updated or explicitly recorded as
no-change-with-reason in a diff-aware contribution manifest.python3 tools/check_contributor_contract.py --base BASE_COMMIT
python3 tools/bandit.py check
python3 website/scripts/build_site.py --lean-verified
python3 website/scripts/check_site.py
git diff --checkContributor/Codex contract ↗ · Theorem publication protocol ↗ · Functor Hypergraph →
Community contribution registry
Loading the public registry…
Credit, review, and governance
Credit travels with the lemma
Contributor name, preferred credit, source provenance, and review history remain in the packet and the eventual teaching note.
Assumptions stay visible
Review may strengthen implementation details, but it must not silently weaken the mathematical target or hide a missing proof behind a theorem card.
Maintainers decide integration
Public proposals are open; core-library integration follows mathematical review, namespace and API review, license checks, and the repository's Lean gate.