ABRL: A Source-Aligned Lean 4 Proof Atlas for Bandit and Reinforcement Learning Theory

Understanding a new bandit or reinforcement-learning result requires identifying which arguments are inherited, which assumptions change, and which proof obligations remain unmatched. We present BanditRLlib, a source-aligned Lean 4 library organized as a proof atlas for this comparison, within the ABRL project. The library formalizes a classical bandit backbone, five end-to-end setting extensions, and a known-reward Hoeffding UCB-VI development, pairs each source-facing theorem with a plain-language proof and its exact Lean declaration, and exposes two complementary views: a compiler-derived dependency graph showing what is formally reused, and a map of conceptual correspondences across settings recorded separately from checked reuse. Two results illustrate the atlas. Heavy-tailed and causal bandits reuse the same two concentration lemmas, called by name, while sharing neither policy nor criterion. A countable-node kernel adapter for hierarchical optimistic optimization removes an extraneous measurability premise introduced by our initial formalization, without changing the source's scope, and a finite certificate shows that a printed pull-count coefficient in the heavy-tailed source fails, with an amended bound proved for the unchanged policy. Source correspondence is reviewed and recorded for every source-facing statement through source-blind reconstruction and explicit discrepancy records. The result is a checked reference frame for reading new work against classical theory: what is inherited, what is recombined, and what remains to be proved. The library, its records, and its tools are available at https://anonymous.4open.science/r/peer-review-artifact-2027.