AutoSamplingTheory.Automation
20 named declarations scanned from AutoSamplingTheory/Automation.lean.
Declarations
inductive AutoSamplingTheory.AutomationStage Compiled Not mapped
No declaration docstring.
inductive AutomationStage where
| sourceIndex
| formalSpec
| leanStatements
| proofSearch
| review
| documented
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:5published source at 77184245109a
inductive AutoSamplingTheory.TaskKind Compiled Not mapped
No declaration docstring.
inductive TaskKind where
| paperReproduction
| exploratoryProof
| lemmaRepair
| sourceAudit
| proofExport
| openProblemProposal
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:14published source at 77184245109a
inductive AutoSamplingTheory.TaskStatus Compiled Not mapped
No declaration docstring.
inductive TaskStatus where
| planned
| active
| blocked
| indexed
| leanCompiles
| merged
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:23published source at 77184245109a
inductive AutoSamplingTheory.AgentRole Compiled Not mapped
No declaration docstring.
inductive AgentRole where
| upper
| middle
| lower
| reviewer
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:32published source at 77184245109a
structure AutoSamplingTheory.AcceptanceGate Compiled Not mapped
No declaration docstring.
structure AcceptanceGate where
name : String
command : String
required : Bool
note : String
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:39published source at 77184245109a
structure AutoSamplingTheory.ArtifactSpec Compiled Not mapped
No declaration docstring.
structure ArtifactSpec where
path : String
language : ArtifactLanguage
purpose : String
mustCompile : Bool
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:46published source at 77184245109a
structure AutoSamplingTheory.AutomationTask Compiled Not mapped
No declaration docstring.
structure AutomationTask where
id : String
title : String
kind : TaskKind
status : TaskStatus
stage : AutomationStage
mode : String
source : String
targetLean : String
artifacts : List ArtifactSpec
gates : List AcceptanceGate
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:53published source at 77184245109a
structure AutoSamplingTheory.AgentContract Compiled Not mapped
No declaration docstring.
structure AgentContract where
role : AgentRole
responsibility : String
writes : List String
mustLogTrial : Bool
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:66published source at 77184245109a
inductive AutoSamplingTheory.PostCycleArtifactKind Compiled Not mapped
No declaration docstring.
inductive PostCycleArtifactKind where
| chineseSummary
| chatgptProPrompt
| retrievalIndex
| technicalReportUpdate
| verifierFeedback
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:73published source at 77184245109a
structure AutoSamplingTheory.PostCycleArtifactSpec Compiled Not mapped
No declaration docstring.
structure PostCycleArtifactSpec where
kind : PostCycleArtifactKind
pathPattern : String
selfContainedForExternalModel : Bool
note : String
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:81published source at 77184245109a
structure AutoSamplingTheory.WorkflowCheckSpec Compiled Not mapped
No declaration docstring.
structure WorkflowCheckSpec where
name : String
checks : List String
inspiredBy : String
note : String
deriving Repr, DecidableEqAutoSamplingTheory/Automation.lean:88published source at 77184245109a
def AutoSamplingTheory.leanBuildGate Compiled Not mapped
No declaration docstring.
def leanBuildGate : AcceptanceGate where
name := "Lean build"
command := "lake exe cache get && lake build && lake build Tests"
required := true
note := "Every automation run must preserve the Lean build."AutoSamplingTheory/Automation.lean:95published source at 77184245109a
def AutoSamplingTheory.forbiddenPatternGate Compiled Not mapped
No declaration docstring.
def forbiddenPatternGate : AcceptanceGate where
name := "No fake proof closures"
command := "rg -n \"\\bsorry\\b|\\badmit\\b|\\baxiom\\b|Prop := True|:= trivial\" AutoSamplingTheory Tests || true"
required := true
note := "Mathematical content must be obligations or real proofs, not fake closures."AutoSamplingTheory/Automation.lean:101published source at 77184245109a
def AutoSamplingTheory.defaultGates Compiled Not mapped
No declaration docstring.
def defaultGates : List AcceptanceGate := [leanBuildGate, forbiddenPatternGate]AutoSamplingTheory/Automation.lean:107published source at 77184245109a
def AutoSamplingTheory.postCycleArtifactSpecs Compiled Not mapped
No declaration docstring.
def postCycleArtifactSpecs : List PostCycleArtifactSpec :=
[
{
kind := PostCycleArtifactKind.chineseSummary
pathPattern := "paper-notes/SALD/markdown/cycle-summaries/latest.md"
selfContainedForExternalModel := false
note := "Human-facing Chinese source audit for the latest long SALD run."
},
{
kind := PostCycleArtifactKind.chatgptProPrompt
pathPattern := "runs/pro-prompts/<task-id>-latest.md"
selfContainedForExternalModel := true
note := "Prompt assumes ChatGPT Pro cannot read local files."
},
{
kind := PostCycleArtifactKind.retrievalIndex
pathPattern := "research-wiki/retrieval-index/<task-id>.json"
selfContainedForExternalModel := false
note := "Compact upper/middle memory for the next cycle."
},
{
kind := PostCycleArtifactKind.technicalReportUpdate
pathPattern := "paper-notes/project-paper/cycle-updates/<task-id>-latest.tex"
selfContainedForExternalModel := false
note := "Middle-agent article update; must separate SALD contributions from external technical lemmas."
}
]AutoSamplingTheory/Automation.lean:109published source at 77184245109a
def AutoSamplingTheory.workflowCheckSpecs Compiled Not mapped
No declaration docstring.
def workflowCheckSpecs : List WorkflowCheckSpec :=
[
{
name := "Blueprint DAG refinement"
checks := ["active source leaf recorded", "solved nodes preserved", "failed route classified"]
inspiredBy := "arXiv:2606.06468"
note := "Goedel-Architect-like blueprint control, specialized to sampling/SDE proof leaves."
},
{
name := "Agent trajectory audit"
checks := ["required artifacts exist", "role handoff recorded", "stale technical-lemma route not reassigned unchanged"]
inspiredBy := "arXiv:2606.06523"
note := "Lean4Agent-like workflow verification; separate from the sampling theorem."
}
]AutoSamplingTheory/Automation.lean:137published source at 77184245109a
def AutoSamplingTheory.threeLayerAgentContracts Compiled Not mapped
No declaration docstring.
def threeLayerAgentContracts : List AgentContract :=
[
{
role := AgentRole.upper
responsibility := "Choose mode, objective, non-goals, dynamic leaf or illness area, and compress LBG-style memory for the next proof cycle."
writes := ["runs/<run-id>/10_upper_director.md", "runs/<run-id>/90_handoff.md"]
mustLogTrial := true
},
{
role := AgentRole.middle
responsibility := "Maintain LaTeX/Markdown/Lean conversion, SLT reuse audit, proof obligations, and lower-ready packets."
writes := ["conversion-windows/", "proof-obligations/", "research-wiki/cited-results/"]
mustLogTrial := true
},
{
role := AgentRole.lower
responsibility := "Attempt one Lean declaration, proof block, source-index repair, proof-obligation refinement, or exploratory candidate route."
writes := ["AutoSamplingTheory/", "Tests/", "proof-attempts/", "candidate-populations/"]
mustLogTrial := true
},
{
role := AgentRole.reviewer
responsibility := "Independently audit build gate, hidden assumptions, source correspondence, SLT port correctness, and faithful/exploratory mode discipline."
writes := ["reviews/", "runs/<run-id>/dialogue.md"]
mustLogTrial := true
}
]AutoSamplingTheory/Automation.lean:153published source at 77184245109a
def AutoSamplingTheory.conversionArtifacts Compiled Not mapped
No declaration docstring.
def conversionArtifacts (stem : String) : List ArtifactSpec :=
[
{
path := "tasks/" ++ stem ++ ".md"
language := ArtifactLanguage.markdown
purpose := "Task contract and progress log."
mustCompile := false
},
{
path := "conversion-windows/" ++ stem ++ ".md"
language := ArtifactLanguage.markdown
purpose := "Synchronized source/Lean/proof-obligation map."
mustCompile := false
},
{
path := "AutoSamplingTheory/" ++ stem ++ ".lean"
language := ArtifactLanguage.lean
purpose := "Lean statement layer or formalized proof blocks."
mustCompile := true
}
]AutoSamplingTheory/Automation.lean:181published source at 77184245109a
def AutoSamplingTheory.seedAutomationTasks Compiled Not mapped
No declaration docstring.
def seedAutomationTasks : List AutomationTask :=
[
{
id := "ASTIS-SALD-001"
title := "Faithfully reproduce the original VA-SALD paper proofs"
kind := TaskKind.paperReproduction
status := TaskStatus.active
stage := AutomationStage.sourceIndex
mode := "faithfulPaper"
source := "/home/nitanda_sub/mark/repos/sald/paper excluding sald_version_2.tex"
targetLean := "AutoSamplingTheory/SALD.lean"
artifacts := conversionArtifacts "SALD"
gates := defaultGates
},
{
id := "ASTIS-RMFLD-001"
title := "Index and validate current RMFLD exploratory proof routes"
kind := TaskKind.exploratoryProof
status := TaskStatus.planned
stage := AutomationStage.sourceIndex
mode := "exploratoryProof"
source := "/home/nitanda_sub/mark/repos/RMFLD/RMFLD_paper"
targetLean := "AutoSamplingTheory/RMFLD.lean"
artifacts := conversionArtifacts "RMFLD"
gates := defaultGates
}
]AutoSamplingTheory/Automation.lean:203published source at 77184245109a
def AutoSamplingTheory.automationTaskCount Compiled Not mapped
No declaration docstring.
def automationTaskCount : Nat := seedAutomationTasks.length
end AutoSamplingTheoryAutoSamplingTheory/Automation.lean:231published source at 77184245109a