production module

`AutoSamplingTheory.Core`

10 named declarations scanned from AutoSamplingTheory/Core.lean.

Imports

Std external

Imported by

AutoSamplingTheoryAutoSamplingTheory.AutomationAutoSamplingTheory.LiteratureAutoSamplingTheory.OpenProblemsAutoSamplingTheory.ProbabilityAutoSamplingTheory.TechnicalLemmas.Registry

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

inductive AutoSamplingTheory.ArtifactLanguage Compiled Not mapped

No declaration docstring.

inductive ArtifactLanguage where
  | lean
  | latex
  | markdown
  | json
  | csv
deriving Repr, DecidableEq

AutoSamplingTheory/Core.lean:14published source at 77184245109a

inductive AutoSamplingTheory.ProofStatus Compiled Not mapped

No declaration docstring.

inductive ProofStatus where
  | planned
  | sourceCited
  | contractOnly
  | obligation
  | formalized
  | blocked
deriving Repr, DecidableEq

AutoSamplingTheory/Core.lean:22published source at 77184245109a

inductive AutoSamplingTheory.SourceKind Compiled Not mapped

No declaration docstring.

inductive SourceKind where
  | paper
  | localTex
  | externalLean
  | mathlib
  | citedResult
  | experimentNote
deriving Repr, DecidableEq

/-- Stable pointer to the source of a mathematical claim. -/

AutoSamplingTheory/Core.lean:31published source at 77184245109a

structure AutoSamplingTheory.SourceAnchor Compiled Not mapped

- Stable pointer to the source of a mathematical claim.

structure SourceAnchor where
  key : String
  kind : SourceKind
  pathOrUrl : String
  label : String
  note : String
deriving Repr, DecidableEq

/-- An honest record for content that is not yet proved in Lean. -/

AutoSamplingTheory/Core.lean:41published source at 77184245109a

structure AutoSamplingTheory.ProofObligation Compiled Not mapped

- An honest record for content that is not yet proved in Lean.

structure ProofObligation where
  id : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
  dependsOn : List String := []
  note : String := ""
deriving Repr, DecidableEq

/-- Paper theorem or lemma translated into a Lean-facing contract. -/

AutoSamplingTheory/Core.lean:50published source at 77184245109a

structure AutoSamplingTheory.TheoremContract Compiled Not mapped

- Paper theorem or lemma translated into a Lean-facing contract.

structure TheoremContract where
  id : String
  title : String
  mode : String
  source : SourceAnchor
  targetLean : String
  statementSummary : String
  proofStatus : ProofStatus := ProofStatus.contractOnly
  obligations : List ProofObligation := []
deriving Repr, DecidableEq

/-- A reusable proof-DAG block, usually one node in a paper proof. -/

AutoSamplingTheory/Core.lean:60published source at 77184245109a

structure AutoSamplingTheory.ProofDagBlock Compiled Not mapped

- A reusable proof-DAG block, usually one node in a paper proof.

structure ProofDagBlock where
  id : String
  interface : String
  source : SourceAnchor
  targetLean : String
  dependsOn : List String := []
  reusedBy : List String := []
  status : ProofStatus := ProofStatus.planned
deriving Repr, DecidableEq

/-- Patterns that are not allowed to close mathematical content. -/

AutoSamplingTheory/Core.lean:72published source at 77184245109a

def AutoSamplingTheory.forbiddenProofPatterns Compiled Not mapped

- Patterns that are not allowed to close mathematical content.

def forbiddenProofPatterns : List String :=
  ["sorry", "admit", "axiom", "Prop := True", ":= trivial"]

AutoSamplingTheory/Core.lean:83published source at 77184245109a

def AutoSamplingTheory.sourceAnchor Compiled Not mapped

No declaration docstring.

def sourceAnchor (key kind pathOrUrl label note : String) : SourceAnchor where
  key := key
  kind :=
    match kind with
    | "paper" => SourceKind.paper
    | "localTex" => SourceKind.localTex
    | "externalLean" => SourceKind.externalLean
    | "mathlib" => SourceKind.mathlib
    | "citedResult" => SourceKind.citedResult
    | _ => SourceKind.experimentNote
  pathOrUrl := pathOrUrl
  label := label
  note := note

AutoSamplingTheory/Core.lean:86published source at 77184245109a

def AutoSamplingTheory.localTexAnchor Compiled Not mapped

No declaration docstring.

def localTexAnchor (key path label note : String) : SourceAnchor :=
  sourceAnchor key "localTex" path label note

end AutoSamplingTheory

AutoSamplingTheory/Core.lean:100published source at 77184245109a