Lean module · Frontier
BanditRLProof.OpenProblems
Open problem registry
Module map
Imports
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
inductive
BanditRLProof.ProblemArea
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.ProblemAreaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
inductive ProblemArea where
structure
BanditRLProof.OpenProblem
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.OpenProblemReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure OpenProblem where
def
BanditRLProof.seedOpenProblems
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.seedOpenProblemsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def seedOpenProblems : List OpenProblem