Posed → progress → resolution → formalization
Source-traceable open-problem history. Core Bandit/RL problems are separated from adjacent Online Learning/optimization/statistics routes. A record may be currently open, partially resolved, resolved, negatively resolved, or resolved with an external formalization. Missing Lean code is tracked separately from mathematical openness.
An old open-problem paper is discovery evidence, not proof that the problem is still open. Current closure status is dated and source-traceable; external/preprint/peer-reviewed resolutions stay distinct. Missing local Lean code is tracked separately.
These questions change a Bandit or reinforcement-learning theorem contract directly.
P0 · resolved-formalized-external
Best-arm identification / pure exploration
Posed by. Lijie Chen and Jian Li · 2016
Local Lean. bridge-only
Graph delta. Adds a BAI-specific information-complexity branch: gap groups → normalized complexity masses → entropy; permutation-averaged instance benchmark; measurable adaptive sampling/stopping; lower-bound change-of-measure; universal algorithm; policy-representation equivalences.
P0 · resolved-negative-preprint
Best-arm identification / fixed budget
Posed by. Chao Qin · 2022
Local Lean. planned
Graph delta. A negative-resolution case should connect oracle allocation geometry, change of measure and impossibility of one uniform instance-complexity functional.
P0 · resolved-preprint
Heavy-tailed bandits / parameter-free learning
Posed by. Gianmarco Genalti and Alberto Maria Metelli · 2025
Local Lean. P0-candidate
Graph delta. High-value bridge from robust mean estimation/concentration to bandit regret, with lower-bound adaptation tradeoffs and scheduled exploration.
P1 · resolved-peer-reviewed
Contextual bandits
Posed by. Alekh Agarwal, Akshay Krishnamurthy, John Langford, Haipeng Luo and Robert E. Schapire · 2017
Local Lean. planned
Graph delta. Useful historical shortcut case: policy-space augmentation changes how first-order online-learning machinery reaches contextual partial feedback.
P1 · partial-current-audit
Contextual bandits / model selection
Posed by. Dylan J. Foster, Akshay Krishnamurthy and Haipeng Luo · 2020
Local Lean. planned
Graph delta. Connects contextual-bandit regret to nested classes, misspecification tests, bias/variance adaptation and impossibility nodes.
P0 · source-open-current-audit
Kernel / RKHS bandits
Posed by. Sattar Vakili, Jonathan Scarlett and Tara Javidi · 2021
Local Lean. P0-candidate
Graph delta. Directly asks whether the confidence-sequence node or the algorithm analysis is the bottleneck; ideal for proof-graph diagnosis across GP-UCB/GP-TS/kernel RL.
P0 · source-open-current-audit
Kernel / RKHS bandits
Posed by. Sattar Vakili · 2022
Local Lean. P0-candidate
Graph delta. Separates deterministic approximation/interpolation error from statistical confidence; likely cross-pollination with numerical approximation and RKHS geometry.
P1 · source-open-current-audit
Privacy / linear contextual bandits
Posed by. Achraf Azize and Debabrota Basu · 2024
Local Lean. planned
Graph delta. Adds privacy accounting/noise geometry on top of self-normalized linear-bandit confidence and regret lower bounds.
P0 · source-open-current-audit
Kernel reinforcement learning
Posed by. Sattar Vakili · 2024
Local Lean. P0-candidate
Graph delta. Natural bridge between the RKHS-confidence frontier and the finite-horizon RL confidence/optimism graph already present in BanditRLlib.
P0 · resolved-peer-reviewed
Distributional / high-probability regret
Posed by. Tor Lattimore and Csaba Szepesvari · 2020
Local Lean. existing-case
Graph delta. Already an excellent internal historical frontier: lower-tail spine is local; the 2026 EQO+ upper route remains a formalization leaf.
P1 · resolved-peer-reviewed
Dynamic / linear bandits
Posed by. Long-standing literature problem (source chain to be frozen before theorem-level port)
Local Lean. planned
Graph delta. Connects dynamic-regret comparator complexity, parameter-free meta-combination and linear-bandit geometry.
P2 · audit-needed
POMDP / planning
Posed by. Kamyar Azizzadenesheli, Alessandro Lazaric and Animashree Anandkumar · 2016
Local Lean. defer-until-RL-route
Graph delta. RL-side computational frontier: nonconvex planning and partial observability rather than statistical regret alone.
P1 · audit-needed
Reinforcement learning / lower bounds
Posed by. Nan Jiang and Alekh Agarwal · 2018
Local Lean. planned
Graph delta. High-value lower-bound bridge for the RL book: separates horizon dependence from assumptions that can hide it.
P2 · audit-needed
Safe / risk-sensitive bandits
Posed by. Filipo S. Perotto, Mathieu Bourgais, Bruno C. Silva and Laurent Vercouter · 2019
Local Lean. planned
Graph delta. Combines multi-objective reward/safety, absorbing ruin events and budget dynamics; good candidate for safe-bandit cross-pollination.
P2 · resolved-peer-reviewed
Adversarial bandits / expert advice
Posed by. Seldin et al. (COLT 2013 open problem) · 2013
Local Lean. low-priority-history
Graph delta. Compact historical example of a resource-constrained information interface producing a matching minimax scale.
P0 · resolved-preprint
Quantum multi-armed / linear bandits
Posed by. Zongqi Wan, Zhijie Zhang, Tongyang Li, Jialin Zhang and Xiaoming Sun · 2023
Local Lean. P0-cross-library-candidate
Graph delta. Quantum-access lower-bound bridge: a high-confidence single-arm quantum testing lower bound via the polynomial method and a Remez-type inequality is lifted by a bandit-to-testing reduction to QMAB, with a linear embedding for QLB. The eventual Lean route should reuse ABRL lower-bound/testing structure and source quantum semantics/testing primitives from ASPBE or audited quantum Lean libraries through an explicit adapter.
These are useful to ABRL, but their mathematical contract belongs to Online Learning, optimization, statistics, games, or another cross-library route. They are intentionally not counted as core Bandit/RL open problems.
P2 · source-open-current-audit
Online learning / sparse linear prediction
Posed by. Manfred K. Warmuth and Ehsan Amid · 2023
Local Lean. route-to-online-learning
Graph delta. Adjacent Online Learning bridge: sparse multiplicative updates / relative-entropy regularization versus closed-form least-squares-style priming. The core question is online regret, so it belongs to the Online Learning book and the technique/Functor graph rather than the core Bandit/RL frontier.
We record collections that were checked even when they contribute zero core Bandit/RL questions. This prevents “not listed” from being confused with “not audited”.
screened 2026-09-19
Core Bandit/RL items: 0 · Adjacent routed items: 2
Freeze the primary problem statement, current resolution evidence, publication status, exact Lean status and expected graph delta. Then use the same contributor contract as theorem work; a missing formalization must never be relabelled as a literature-open theorem.
Contributor/Codex contract →