Bandit Book
Ten core teaching routes plus source Chapters 13–17. Broader Bandit classification, techniques, theorem-level bounds and research frontiers are separate linked views rather than pseudo-chapters.
Bandit Algorithms
Verified bandit and reinforcement-learning theory in Lean
BanditRLlib
Learn bandit and reinforcement-learning theory beside its compiled Lean interfaces, search exact declarations, and contribute one reviewable lemma at a time.
Paper. ABRL: A Target-Faithful Autoformalization Harness and Lean 4 Library for Bandit and Reinforcement Learning Theory
GitHub repository ↗Compare minimax frontiersLocal experimental workspace
Choose your path
BanditRLlib, three ways to use it
Books · shared Lean foundations
Choose a book. Follow the same mathematics.
Each book is a reading view of one Lean library. Source mapping and local proof status remain explicit.
Reinforcement Learning Book
A dedicated RL reading view. Existing finite-horizon material is available; mapping the new source is planned.
Reinforcement Learning: Theory and Algorithms
Online Learning Book
Convex optimization and regret minimization. Existing EXP3/FTRL routes are shared references; adjacent online-learning frontier questions are indexed separately from core Bandit/RL open problems.
Online Learning: A Modern Introduction Using Convex Optimization
Conformal Prediction Book
Reserved for a dedicated conformal prediction curriculum. Source selection and theorem mapping await review.
Source selection pending
Bandit Book contentsTeaching routes · source chapters · coverage
Chapter-by-chapter source spine · Chapters 13–17
Part IV: Lower Bounds
Follow the proof technology from basic lower-bound ideas through information theory, minimax bounds, instance-dependent bounds, and high-probability bounds. Each chapter links its exact source scope to Lean declarations.
What completion means. The five recorded chapter contracts have prior merged compilation evidence; this build’s banner reports whether the gate was rerun, not the entire textbook or every exercise. Chapter 17 formalizes an explicitly corrected version: Claim 17.6 uses the event
T_i ≤ n/2, and Theorem 17.4 assumes 0 < δ ≤ 1/32, with constants c = 1/160 and C = 64. See the chapter pages for assumptions, source differences, and optional work.
Chapter 13
Compiled
Lower Bounds: Basic Ideas
155–159 print · 189–194 PDF
Read the exact scope, proofs, and remaining optional work.
Chapter 14 Compiled Foundations of Information Theory 160–169 print · 195–206 PDFRead the exact scope, proofs, and remaining optional work.
Chapter 15 Compiled Minimax Lower Bounds 170–176 print · 207–214 PDFRead the exact scope, proofs, and remaining optional work.
Chapter 16 Compiled Instance-Dependent Lower Bounds 177–184 print · 215–223 PDFRead the exact scope, proofs, and remaining optional work.
Chapter 17 Compiled High-Probability Lower Bounds 185–190 print · 224–230 PDFRead the exact scope, proofs, and remaining optional work.
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.
1. Finite bandits, traces, and regret
Ch. 1 and Ch. 4, especially §4.5 · online pp. 8–16 and 56–69; regret decomposition pp. 62–63
2. Probability, kernels, filtrations, and concentration
Ch. 2, Ch. 3, and Ch. 5 · online pp. 18–42, 46–54, and 74–81
3. Explore-Then-Commit
Ch. 6 · online pp. 91–96
4. UCB: confidence events to regret
Ch. 7; KL-UCB extension in Ch. 10 · online pp. 102–111; KL-UCB pp. 133–141
5. OFUL, self-normalized confidence, and stopping times
Ch. 19–20; stopping times in §3.3 · online pp. 238–262; stopping-time basics pp. 50–54
6. Thompson sampling and Bayesian regret
Ch. 34 and Ch. 36 · online pp. 421–436 and 460–475
7. EXP3 and adversarial concentration
Ch. 11–12 · online pp. 148–172
8. Tsallis-FTRL, corruption, and nonstationarity
Ch. 28 (FTRL and mirror-descent foundation) · online pp. 327–344
9. Finite-horizon reinforcement learning
Ch. 38 · online pp. 512–538
10. Automation, resources, and open routes
Parts VII–VIII as a background index · online pp. 358–538
Current evidence snapshot
What is available now—and what is still open
6847b678a73d ↗
These cards are generated from the Lean index, teaching crosswalks, implementation ledger, and harness-comparison log. They are not hand-entered completion percentages.
Lean snapshotCompiled
10,434
indexed declarations
796 modules · 7,689 theorems and lemmas · 0 declarations with sorry or admit.
Teaching layerSource mapped
10
Book Map chapters
14 source-theorem restatements and 5 Part-IV chapter pages connect algorithms, page references, mathematics, and Lean.
Follow a reading route →Harness comparisonPrototype
0/2
matched experiments
Decision: insufficient evidence. The default is retained; the next evidence-gathering arm is hierarchical.
Active theorem frontierPartial
SGB Theorem-2 follow-on
First named open bridge. A bridge from the compiled terminal-count-below event to a fixed-cutoff starvation trigger/event; the exact probability split and missing-pull-to-terminal-count inclusion do not supply occurrence-conditioned IID.
Open evidence and remaining gaps →Powered by two connected systems
One engine produces verified mathematics; one library makes it reusable.
ABRL Adaptive Harness
A fixed mathematical target enters an evidence-aware scheduler. The hierarchical route remains the default; bounded master–worker trials use the same hashed route packet, and only separate reviewer verdicts can enter the comparison.
Inspect the ABRL harness →BanditRLlib
Compiled Lean declarations → searchable reusable library → textbook-aligned learning → LaTeX↔Lean formalization → community lemma intake.
Browse BanditRLlib →flowchart LR
Target["Frozen mathematical target<br/>paper, textbook, or proposal"] --> Scheduler["Evidence-aware scheduler<br/>same target, budget, and source packet"]
subgraph Harness["ABRL · adaptive autoformalization harness"]
Scheduler --> Hierarchy["Hierarchical default<br/>director → planner → one Lean leaf"]
Scheduler -. "bounded experiment" .-> Parallel["Master–worker trial<br/>independent proof routes"]
Hierarchy --> Gate["Common Lean + reviewer gate<br/>certificate, blocker, reuse"]
Parallel --> Gate
Gate -. "matched log and diagnostics" .-> Scheduler
end
Gate -->|accepted declarations| Library["BanditRLlib<br/>verified Lean library"]
Library --> Learn["Learn<br/>source-mapped Book Map"]
Library --> Reuse["Reuse<br/>declarations + proof graph"]
Library --> Formalize["Formalize<br/>local experimental workspace"]
Library --> Contribute["Contribute<br/>reviewed lemma packets"]
Formalize -. "candidate packet" .-> Target
Contribute -. "proposal packet" .-> Target
Project scope and completion boundariesLive inventory · project purpose
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.
796Lean source modules, including the root aggregator
10,434Indexed definitions, structures, theorems, and lemmas
7,689Theorems and lemmas
0Declarations containing
sorry or admitTwo levels of completion. A local declaration can compile while a broader textbook or upstream-compatible route remains partial. The site reports both levels separately; theorem cards and paper references are never counted as local proofs.
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.
Identity boundary. ABRL is the proving system and research project. BanditRLlib is the verified Lean library, website, formalization workspace, and contribution interface produced by that system.
Upper bounds · lower bounds · local Lean evidence
BanditRLwiki: compare results under the same assumptions
The research atlas currently indexes 13 theorem-comparison cases across 7 assumption families. Each case fixes its reward model, feedback, horizon, regret notion, and salient parameters before comparing rates. Published optimality, theorem-level source audit, and local Lean compilation are three independent ledgers.
Find the best compatible upper and lower theorem
Open a setting, inspect the precise comparison signature, follow primary-paper links, and see every remaining logarithmic, constant, parameter, or model-class mismatch.
Open BanditRLwiki →Separate open mathematics from open formalization
1 case remains in the source-audit queue. The Frontier never turns a missing reference into a literature-open claim, and every Lean blocker names the exact missing bridge.
Inspect frontier leaves →More project pathsContributors · installation
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.
Bo Xue
Project author
Project author.
Atsushi Nitanda
Project author
Project author.
Hau-San Wong
Project author
Project author.
Qingfu Zhang
Project author
Project author.
Reproduce the formalization
Installation
Install Lean
Install Git, Python 3, and Lean through Elan. The repository pins leanprover/lean4:v4.29.1.
Clone the repository
git clone https://github.com/DakeBU/Auto-Bandit-RL-Proof-In-Sleep.git
cd Auto-Bandit-RL-Proof-In-SleepRun the proof gate
lake update
python3 tools/bandit.py checkA reviewable path into the library
How to contribute
- Choose one claim.Start from a book, paper, proof gap, or existing chapter and record the exact source and assumptions.
- Agree on the statement.Open a lemma proposal before a large formalization so scope, namespace, and dependencies can be reviewed.
- Compile and explain.Add the Lean declaration, tests, plain-English statement, proof idea, and an honest status.
- Submit for integration.The project gate and maintainer review decide when a result becomes indexed as compiled.
Research details and local toolsProgress · reading routes · Live Formalization
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" : 86 "Partial route" : 8 "Planned" : 1 "Blocked" : 2 "Stated, proof incomplete" : 0
Choose a mathematical route
Five reading paths through the same library
Each route reuses the common foundations but emphasizes a different proof technology. These are pedagogical paths, not additional completion claims.
Stochastic finite arms
Start with bookkeeping, add concentration, then compare ETC and optimism.
Linear and contextual
Build the probability interface before moving from optimism to confidence ellipsoids.
Bayesian
Use the common probability layer, then follow posterior sampling and its information route.
Adversarial and OCO
Move from importance weighting in EXP3 to regularized FTRL and Tsallis geometry.
Finite-horizon RL
Reuse probability and optimism interfaces before entering Bellman recursion and UCBVI.
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.
Static-site boundary. GitHub Pages does not compile Lean or send source to a hosted proving service. Compilation and provider-backed formalization require the explicitly started loopback-only local companion server.