Component · spec & evidence

Verifier Lab Kernel

Folds nine proof checks into one report labeling each line by which source actually backs it.

Contract

Does This assembly point for the Lean/proof toolkit runs nine smaller formal-math pipeline checkers together and folds their results into one leak-proof report that labels every line by where it came from: a Lean verifier, an answer-key (oracle) comparator, an AI suggestion, a retrieval miss, or a row thrown out for breaking the rules. The report carries only references, hashes, counts, and verdicts, never the actual proof text, AI output, or answer-key bodies. One result record shows which claims a Lean verifier actually backed versus which are just hints or were rejected, instead of leaving a pile of separate outputs to be taken on faith.

Scope limit It validates the declared public contract shape of the proof packet and component result records only; it does not establish anything correct, count oracle/provider output as forward proof success, import private or Mathlib-dependent proof bodies, use external model services, change source files, or claim benchmark solve rates, launch, or maturity.

Run

PYTHONPATH=src python3 -m microcosm_core.organs.verifier_lab_kernel run --input fixtures/first_wave/verifier_lab_kernel/input --out receipts/first_wave/verifier_lab_kernel

Evidence

ClassContract validatorevidence 5/5Import validation

Links to Corpus Readiness Mathlib Absence Gate, Lean Std Premise Index, Formal Math Premise Retrieval, Tactic Portfolio Availability Probe, Target Shape Tactic Routing Gate, Ring2 Premise Retrieval Precision Recall Harness, Formal Math Verifier Trace Repair Loop, Proof Diagnostic Evidence Spine, Formal Math Lean Proof Witness, Verifier Lab Execution Spine

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module