Unclosed leaves, with the reason visible
BanditRLwiki Frontier
A mathematical literature gap is not the same as a missing source audit or a local Lean proof gap. This page keeps all three boundaries explicit.
0literature-open cases
36named formalization leaves
1source-audit cases
13formalization-open cases
Literature-open cases
These are explicit negative findings from the scoped primary-source audit. A missing database entry is never enough to place a case here.
No explicitly audited open leaf is registered.
Source-audit queue
These cases have a strong closest result, but a compatible primary upper/lower theorem pair has not yet been frozen. They are not labeled literature-open.
contextual-finite-policy-exp4pWhich exact contextual lower theorem matches the displayed Exp4.P contract, and how should its policy class be represented in Lean?Source audit pending
Active source ports outside the comparison atlas
These two NeurIPS 2025 ports record current compiled progress and exact nonclaims. One now contains a narrowly scoped compiled paper endpoint, while both remain partial audits and remain outside the minimax ledger until their remaining contracts and compatible comparison partners are frozen.
Source-frozen external audit
Succinct stochastic-bandit lower-bound geometry
A Novel General Framework for Sharp Lower Bounds in Succinct Stochastic Bandits
Guo Zeng and Jean Honorio · 2025
54 named declarations compile in the current library.
Definitions 3.1–3.3, Lemmas 3.1–3.4, the finite-Bessel strict-support route, and a global-R boundedness diagnostic compile.
Boundary. This is a source-frozen partial port, not yet an assumption-matched upper/lower comparison case. Lemmas 3.5–3.6, Assumption 3.7, Theorem 3.8, and every regret endpoint remain uncompiled.
Representative Lean declarations
Source-frozen external audit
Stochastic-gradient bandit Theorem 1, Corollary 1, and blocked Theorem-2 follow-on
Does Stochastic Gradient really succeed for Bandits?
Dorian Baudry, Emmeran Johnson, Simon Vary, Ciara Pike-Burke, and Patrick Rebeschini · 2025
361 named declarations compile in the current library.
The counted SGB audit retains the exact 361 = 223 + 23 + 25 + 26 + 7 + 8 + 13 + 28 + 8 audit-slice inventory through one-step selected-reward freshness, terminal-count events, nth-pull-to-count bridges, and a generic finite-horizon low-count regret consumer. A separate ten-declaration native-law module identifies the complete visible/native trajectory law. The selected-block module now has 36 declarations: eight transport finite optimal-arm pull-time/reward blocks to a masked latent-coupling law with explicit `WithTop Nat` missing pulls, fourteen define and transport the exact finite Appendix-C `S0/S1` event, ten split the pure latent phase probability into the generated all-present event plus an explicit missing-pull event, and four map the missing branch to a low-count event, transport its probability to the generated trajectory, and charge its existing mass against expected sampled pseudo-regret. The exact Theorem-1 and Corollary-1 endpoints use generated zero-initialized two-arm fixed-IID trajectories with a Unit Dirac environment prior; the reward laws themselves remain bounded fixed-IID laws. Corollary 1 assumes T >= 2, 0 < Delta < 1, and one fixed eta_T = sqrt(log T / T) per horizon.
Boundary. The audit remains partial. Corollary 1 is a direct Theorem-1 consumer, not evidence for the polynomial-regret Theorem 2. Complete visible/native law equality, missing-pull-aware selected-block transport, exact finite phase-event transport, the disjoint missing/all-present probability split, the missing-pull-to-terminal-count inclusion, and the missing-pull finite-horizon expected-regret consumer now compile. None is a selected-IID theorem or a positive-probability producer. The next unique leaf is the generated all-present Appendix-C phase trigger at a fixed chronological cutoff; the stopped-prefix future-cylinder law, conditional no-return probability >= 1/2, Rademacher/binomial ballot probability, asymptotic assembly, and the frozen terminal remain blocked. Theorem 4 likewise still lacks the general-K generated process, uniform buffer/survival producer, stopped supermartingale/Doob route, and final regret assembly.
Representative Lean declarations
How a leaf closes
- Freeze the contract.Fix assumptions, regret notion, quantifiers, constants, and source location.
- Audit primary evidence.Record the closest compatible upper and lower theorem; name every mismatch.
- Compile the exact bridge.Close one named proof obligation without adding an unadvertised assumption.
- Pass independent gates.Lean, tests, website links, source review, and deployment evidence must agree before status promotion.