BanditRLlib

Powered by two connected systems

One engine produces verified mathematics; one library makes it reusable.

flowchart LR
    Target["Mathematical target<br/>paper, textbook, or proposal"] --> Upper["ABRL upper layer<br/>planning and target fence"]
    subgraph Harness["ABRL · hierarchical autoformalization harness"]
        Upper --> Middle["middle layer<br/>route and obligation design"]
        Middle --> Lower["lower layer<br/>Lean proof construction"]
        Lower --> Compiler["Lean 4 compiler<br/>lake + Mathlib"]
        Compiler --> Reviewer["reviewer and full gate<br/>statement + evidence audit"]
        Reviewer -. "diagnostics and refinement" .-> Middle
    end
    Reviewer -->|accepted declarations| Library["BanditRLlib<br/>verified Lean library"]
    Library --> Learn["Learn<br/>ten-chapter book map"]
    Library --> Reuse["Reuse<br/>declaration catalogue"]
    Library --> Formalize["Formalize<br/>retrieval-grounded candidates"]
    Library --> Contribute["Contribute<br/>reviewed lemma packets"]
    Formalize -. "candidate packet" .-> Upper
    Contribute -. "proposal packet" .-> Upper

BanditRLlib, three ways to use it

Live source inventory

The numbers below are generated from the current internal BanditRLProof/ namespace at build time. BanditRLlib is the public library name; the mature namespace is intentionally unchanged.

What this project is building

Bandit and reinforcement-learning proofs mix finite combinatorics, probability kernels, conditional expectation, concentration, optimization, and algorithm-specific bookkeeping. ABRL organizes that work into small Lean-checkable leaves. An automated hierarchy proposes and proves leaves; reinforcement-learning ideas help select promising proof routes; bandit objectives allocate effort among those routes; and Lean is the final certificate.

The current tree is no longer only a finite-bandit foundation. It contains concrete ETC, ordinary UCB, a conservative bounded generated KL-UCB route, stationary Thompson, EXP3, and Tsallis endpoints; an OFUL chain reaching self-normalized confidence and one horizon-free policy with all-time, all-horizon, and stopping consumers, plus a separately labeled horizon-indexed expected-consistency family; and a finite-horizon RL development that now reaches a canonical known-reward Hoeffding UCBVI-CH high-probability cumulative episode pseudo-regret theorem and its failure-aware expected consumer on one generated adaptive process. Natural-causal consistency and stopping-time RL remain independent compiled extensions. Bernstein/minimax and stochastic-reward UCBVI, sharp KL-Chernoff and asymptotically optimal KL-UCB refinements, full BwK, preference, federated, and several modern routes remain partial, planned, or blocked at named interfaces.

Formalized textbook map

Book map: ten routes through bandits and RL

The curriculum is anchored in Lattimore and Szepesvári's Bandit Algorithms, with algorithm-specific papers for OFUL, Tsallis-INF, and UCBVI. It is a source-mapped learning path, not a chapter-for-chapter reproduction of one book. Each card reports online-edition pages and the chapter's canonical compiled boundary.

Chapter-by-chapter source spine

Part IV: Lower Bounds

This separate layer follows Chapters 13–17 of Bandit Algorithms in order. It does not change the ten-chapter Book Map or imply that the whole textbook is complete.

Open the Part IV spine

People behind the project

Authors

The project authors are listed separately from future community contributors. Roles are intentionally neutral unless contribution metadata is explicitly recorded.

Meet the contributors

Reproduce the formalization

Installation

git clone https://github.com/DakeBU/Auto-Bandit-RL-Proof-In-Sleep.git
cd Auto-Bandit-RL-Proof-In-Sleep

lake update
python3 tools/bandit.py check

Full installation guide

A reviewable path into the library

How to contribute

1. Choose one claim.Start from a book, paper, proof gap, or existing chapter and record the exact source and assumptions.
2. Agree on the statement.Open a lemma proposal before a large formalization so scope, namespace, and dependencies can be reviewed.
3. Compile and explain.Add the Lean declaration, tests, plain-English statement, proof idea, and an honest status.
4. Submit for integration.The project gate and maintainer review decide when a result becomes indexed as compiled.

Progress without invented percentages

This chart counts the explicit milestones in the website's implementation map. It does not estimate what percentage of all bandit or RL mathematics has been formalized.

pie showData
  title Implementation-map milestones (not a percentage of all mathematics)
  "Compiled local endpoint" : 60
  "Partial route" : 4
  "Planned" : 1
  "Blocked" : 5
  "Stated, proof incomplete" : 0

Recommended reading order

Students can take a short stochastic route through Foundations → Probability → ETC → UCB, a linear route through UCB → OFUL, an adversarial route through EXP3 → Tsallis-FTRL, or continue from Probability and OFUL stopping-time ideas into finite-horizon RL. Thompson sampling branches from posterior kernels.

flowchart LR
  Start["New to Lean or bandit/RL proofs"] --> F["1. Foundations"]
  F --> P["2. Probability layer"]
  F --> ETC["3. ETC"]
  ETC --> UCB["4. UCB"]
  P --> UCB
  UCB --> OFUL["5. OFUL + stopping times"]
  P --> TS["6. Thompson sampling"]
  F --> E["7. EXP3"]
  P --> E
  E --> T["8. Tsallis-FTRL"]
  P --> T
  P --> RL["9. Finite-horizon RL"]
  OFUL --> RL
  UCB --> RL
  RL --> Frontier["10. Frontier + contribution workflow"]
  T --> Frontier
  TS --> Frontier

  IDE["Research IDE: LaTeX ↔ Lean ↔ tree"] -. "use beside every chapter" .-> F
  IDE -.-> RL

BanditRLlib and Live Formalization share one contribution language

The workspace renders editable LaTeX, loads reviewed LaTeX-to-Lean mappings, visualizes declaration dependencies, and can call the pinned Lean compiler through a loopback-only companion server. It can now export a versioned lemma packet for community review; a future authenticated compiler can submit that same packet directly as a proposed contribution.