P0 frontier history · external formalization bridge

Gap-entropy conjecture and almost instance-wise optimal BAI

This page preserves the decade-long problem history and the graph structure introduced by its resolution without pretending that an external Lean project is locally compiled.

Open external Lean graph bridge All frontier histories

Original source problem

Open Problem: Best Arm Identification: Almost Instance-Wise Optimality and the Gap Entropy Conjecture · Lijie Chen and Jian Li · 2016

Open primary source ↗

Progress and resolution

2017. Towards Instance Optimal Bounds for Best Arm Identification — Major partial progress on upper/lower routes.
2026. Gap Entropy and Almost Instance-Wise Optimal Best-Arm Identification — Public manuscript plus Lean 4 formalization by Jiarui Yao, Jiaxi Zhao and Xiangxin Zhou.
2026. A positive resolution of the gap-entropy conjecture — Independent proof by P. M. Aronow, Nathan Kallus and Patrick Lopatto.

Formalization boundary

External status: external-kernel-verified. BanditRLlib local status: bridge-only. The external repository uses Lean 4.33.1; BanditRLlib currently uses Lean 4.29.1.

GapEntropy.gapEntropyConjecture
GapEntropy.universalEntropyUpperBound
GapEntropy.almostInstanceWiseOptimality
GapEntropy.positiveSourceAlmostInstanceWiseOptimality
GapEntropy.PolicyRepresentations.standardBenchmark_eq

Truth boundary. These declaration names are attributed external evidence. They are not local BanditRLlib compiled declarations until a source-faithful toolchain/port decision passes the local project gate.

Why this belongs in the proof graph

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.

The contribution should be audited as possible bridge/hub structure, not merely as one terminal BAI theorem: gap-scale grouping, an order-oblivious benchmark, policy representation, information lower bounds and a universal algorithm sit between generic probability infrastructure and the final sample-complexity claim.