production module

`AutoSamplingTheory.OpenProblems`

3 named declarations scanned from AutoSamplingTheory/OpenProblems.lean.

Imports

AutoSamplingTheory.Core

Imported by

AutoSamplingTheory

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

structure AutoSamplingTheory.OpenProblem Compiled Not mapped

No declaration docstring.

structure OpenProblem where
  id : String
  title : String
  mode : String
  acceptancePredicate : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.planned
deriving Repr, DecidableEq

AutoSamplingTheory/OpenProblems.lean:5published source at 77184245109a

def AutoSamplingTheory.openProblems Compiled Not mapped

No declaration docstring.

def openProblems : List OpenProblem :=
  [
    {
      id := "ASTIS-OPEN-SDE-MEASURE-BACKEND"
      title := "Port or prove the measure-theoretic backend for KL/FI/LSI/Fokker--Planck SALD arguments"
      mode := "shared"
      acceptancePredicate := "Lean declarations for KL/FI/LSI and the differentiation identities used by SALD build without fake proof closures."
      source := {
        key := "sald-original"
        kind := SourceKind.localTex
        pathOrUrl := "/home/nitanda_sub/mark/repos/sald/paper"
        label := "SALD analytic proof backend"
        note := "Use Mathlib and SLT ports where possible."
      }
      status := ProofStatus.planned
    }
  ]

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

def AutoSamplingTheory.openProblemCount Compiled Not mapped

No declaration docstring.

def openProblemCount : Nat := openProblems.length

end AutoSamplingTheory

AutoSamplingTheory/OpenProblems.lean:32published source at 77184245109a