Lean module · Frontier
BanditRLProof.Automation
This file makes the harness roles and artifacts part of the compiled Lean project. It does not run agents; it records the protocol that external agents must satisfy.
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.HarnessProfile
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.HarnessProfileReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
inductive HarnessProfile where
inductive
BanditRLProof.AgentRole
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.AgentRoleReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
inductive AgentRole where
inductive
BanditRLProof.TaskKind
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.TaskKindReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
inductive TaskKind where
inductive
BanditRLProof.TaskStatus
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.TaskStatusReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
inductive TaskStatus where
structure
BanditRLProof.ArtifactSpec
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.ArtifactSpecReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure ArtifactSpec where
structure
BanditRLProof.AcceptanceGate
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.AcceptanceGateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure AcceptanceGate where
structure
BanditRLProof.HarnessTask
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.HarnessTaskReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure HarnessTask where
def
BanditRLProof.defaultLeanGate
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.defaultLeanGateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def defaultLeanGate : AcceptanceGate where
def
BanditRLProof.defaultHarnessProfile
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.defaultHarnessProfileReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def defaultHarnessProfile : HarnessProfile