Lean 4 formalization of the paper Optimal Best Arm Identification with Fixed Confidence (Garivier and Kaufmann, COLT 2016), on top of LMLExplore.

• Blueprint
• Blueprint as pdf
• Dependency graph
• Referee site
• Literature links: which declarations formalize which results of the paper
• Errata: errors found in the paper, with their corrections