BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

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.

Propose a lemma Read the contribution guide Draft in the local experimental workspace

Four steps to a reviewed contribution

  1. Source the mathematics.Name the paper, book, formal proof gap, or original result and state every assumption.
  2. Open a proposal.Agree on the target statement, namespace, module, and dependencies before a large implementation.
  3. Compile and document.Submit Lean code, tests, plain-English meaning, mathematical notation, and proof correspondence.
  4. Pass review and integration.Only the full project gate and maintainer review can mark the declaration integrated and compiled.

Three useful contribution sizes

Level A

Explain or connect

Improve a teaching note, add a literature pointer, identify a missing assumption, or connect an existing declaration to a textbook theorem.

Level B

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.

Level C

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"]
Community contribution loop from sourced mathematics to an integrated Lean declaration · editable Mermaid source
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.

Open the JSON Schema · Open the machine-readable registry

{
  "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.

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.

Governance · Code of Conduct · Open proposals