mm-lean4 formalizes a Metamath verifier in Lean 4. The project includes operational specification and semantic specification. The project includes a proof.
-
Metamath/Spec/Metamath/Spec/holds declarative and operational specifications with equivalence
-
Metamath/Verify.leanMetamath/Verify.leanimplements the verifier
-
Metamath/KernelCorrectness.leanMetamath/KernelCorrectness.leanproves kernel soundness and completeness
-
Metamath/ParserCorrectness.leanMetamath/ParserCorrectness.leanproves parser invariants and correctness layers
-
Metamath/ParserEquivalence.leanMetamath/ParserEquivalence.leanis the canonical review entry point
-
Metamath/PrefixProvability/Checker.leanMetamath/PrefixProvability/Checker.leancertifies prefix provenance per accepted event
-
Metamath/StoredStatementSoundness.leanMetamath/StoredStatementSoundness.leanconnects the full active proof frame to the exact trimmed statement and eliminates earlier$prules by cut
-
Metamath/Spec/Completeness.leanMetamath/Spec/Completeness.leanproves that a statement is provable in Mario Carneiro's declarative semantics iff some extended frame of it has a Metamath proof
-
Metamath/SourceCompleteness.leanMetamath/SourceCompleteness.leanproves that such a statement is provable iff the parser accepts a proof of it in source text, after finitely many fresh dummy declarations, in modes without duplicate$fstatements
-
Metamath/RunEmission.leanMetamath/RunEmission.leanties the emitted chronology to the actualcheckinvocation by refinement and determinism
-
Metamath/IncludeInterpretation.leanMetamath/IncludeInterpretation.leanstates each mode's complete acceptance policy, decomposes its include and compressed-proof dimensions, and connects the declarations to runtime helpers
-
Metamath/ErrorCodeSemantics.leanMetamath/ErrorCodeSemantics.leancertifies everyParseErrorCodeconstructor
-
Metamath/DeclarativeSpec.leanMetamath/DeclarativeSpec.leanhosts Mario Carneiro's declarative specification; the typing premise of itsaxrule ranges over the applied statement's variables, andMetamath/Spec/DeclarativeOriginal.leanproves it equivalent to his original rule on trimmed axiom sets, which translated databases are
-
Metamath/ParserEquivalenceExamples.leanMetamath/ParserEquivalenceExamples.leanprovides compiling usage examples
-
Metamath/CounterexampleInsertError.leanMetamath/CounterexampleInsertError.leanprovides a counterexample for insert-with-error behavior
-
Metamath/ParserSoundnessDemo.leanMetamath/ParserSoundnessDemo.leanis a development artifact
-
Metamath/DeclarativeSpecDemo.leanMetamath/DeclarativeSpecDemo.leanholds Mario Carneiro's by-hand translation ofdemo0.mm
-
Metamath/ZipperTest.leanMetamath/ZipperTest.leanis a development artifact
- The toolchain pins Lean 4.33.1.
- The toolchain pins Batteries at commit
4488d40.
- Sorries are 0.
- No project-declared axioms in active
Metamath/Lean code; the headline theorems depend on Lean's standard axioms (propext,Classical.choice,Quot.sound) under#print axioms. lake buildsucceeds on the pinned toolchain.- The specification suite is 187 of 187 in the default
zarmode. - The fail-closed reference differential attempts all 187 registered databases
in
knifeandexemode. Its report distinguishes semantic verdicts from reference-process failures; a crash is never counted as rejection or agreement. - Direct
set.mmverification reports 67764 objects. - The CLI honesty and resource-bound gates are
scripts/cli_honesty.sh.
rg -n '^\s*sorry\b|by sorry' Metamath/ --glob '*.lean'
lake env lean scripts/print_axioms.lean
MM_LEAN4=.lake/build/bin/mm-lean4 sh scripts/cli_honesty.sh
MM_LEAN4=.lake/build/bin/mm-lean4 \
METAMATH_KNIFE="$METAMATH_KNIFE" METAMATH_EXE="$METAMATH_EXE" \
METAMATH_TEST="$METAMATH_TEST" scripts/reference_mode_differential.shThe development includes end-to-end correctness theorems for the verifier.
The detailed clause and theorem scopes are in docs/SpecTheoremMap.md.
check_storedStatements_writtenProof(in a mode satisfyingIsSound) connects the written$pproof to the exact trimmed statement stored by the include-aware executable.check_every_theorem_provable_from_run_axiom_events(Metamath/RunEmission.lean, in a mode satisfyingIsSound) eliminates prior$prules by chronological cut, leaving only$a-classified events — over the run's own chronology:SinglePassEmissionties the step list to the actual invocation through equations about the entrypoint's own IO recursion, and its determinism theorem (SinglePassEmission.unique) makes that list the only one any emission of the invocation can produce.InsertionHistorysupplies the registry-continuity form of the same history;ExecutionInsertionHistoryis its execution-indexed strengthening (subdatabase, exactly-one creation, and bound payloads over the emitted list).- The
proofChecker_*_in_parsedDBfamily is fixed-final-database adequacy and is not presented as source-proof acceptance. checkBytes_parseErrorCode?_fullyCertifiedcertifies that every decoded error code agrees with its evidence payload.parser_operational_to_frameDerivable_totalandparser_frameDerivable_to_operational_totalare the parser-specialized bridge to derivability by Mario Carneiro's rules in the frame.statementProvable_iff_exists_extendedFrame(Metamath/Spec/Completeness.lean): a stored statement is provable in Mario Carneiro's declarative semantics iff some extended frame of it (the frame plus$fand$dstatements for dummy variables, §4.2.7) has a Metamath proof. At one fixed frame the two differ (Metamath/Spec/FixedFrameCounterexample.lean).statementProvable_iff_sourceAcceptsandstatementProvable_iff_fileAccepts(Metamath/SourceCompleteness.lean): after an error-free read of source text that ends between statements with no token pending, in a mode without duplicate$fstatements (notexeorpermissive), such a statement is provable from the assertions read so far iff the parser accepts a proof of it written after finitely many fresh$v,$fand$ddeclarations;check_accepts_of_statementProvableandstatementProvable_of_checkstate it throughVerify.checkon a root file without includes.
For incomplete proofs, zar accepts ? but reports the database as accepted
and incomplete, never verified. sound and knife reject ?.
Parser success discharges WellFormedDatabaseStrong, FloatVarNoDup, and FrameVarsDisjointConsts.
proofChecker_normal_iff_frameDerivable_in_parsedDB composes the bridge from checkBytes success.
h_success : (checkBytes bytes).error? = none
-> parser_construction_wf_scoped
-> parser_toDatabase_wellFormed_strong
-> floatVarNoDup_of_uniqueFloatVars
-> frameVarsDisjointConsts_of_toFrame
-> operational_to_frameDerivable, frameDerivable_to_proofValid
- Diagnostic taxonomy is
docs/ErrorCodes.md. - The specification-to-theorem map is
docs/SpecTheoremMap.md. - The verifier reports the first error.
- Include I/O failures are environment errors.
- Verifier modes are distinct specifications.
Metamath/IncludeInterpretation.leandeclares and connects the distinctzar,knife, andexepolicies. The reference differential compares semantic acceptance verdicts and fails closed on reference-process crashes.- Every mode but
permissivefollows the book's comment rules (§4.1.1–4.1.2), andexeadditionally treats vertical tab as whitespace, as metamath.exe does;permissiveignores comment text up to the first standalone$). Every mode lets a variable take different$ftypes in separate scopes; each stored assertion keeps its own frame. - Two operational resource bounds exist that the Metamath specification does
not impose:
maxIncludeDepth(default 100) andmaxIncludeResolutions(default 1000000, the include-driver loop's resolution budget; duplicate suppressions also consume one resolution). Exceeding either is reported loudly under theimpl_resourceBoundclause — an implementation resource outcome, not a claim that the source violated section 4.1.2. --max-include-resolutions=Noverrides the resolution budget;scripts/cli_honesty.shpins the zero/sufficient/default canaries.- Unknown, malformed or conflicting command-line options are rejected with exit code 2.
- Formal theorems cover both the pure
checkByteslane overByteArrayinput and properties derived by induction over the include-awarecheckimplementation;Metamath/RunEmission.leanties them to the invocation's own emitted chronology. - The active executable frontend is single-pass and include-aware.
Metamath/FrontendBridge.leanconnects frontend outcomes back to the reviewed theorem chain.Metamath/ParserEquivalence.leanis the review entry module for the composed chain.
METAMATH_TEST is a checkout of the specification suite: https://github.com/zariuq/metamath-test, branch unit-tests.
ROOT="$(pwd)"
lake build
MM_LEAN4="$ROOT/.lake/build/bin/mm-lean4" sh scripts/cli_honesty.sh
(cd "$METAMATH_TEST" && \
MM_LEAN4="$ROOT/.lake/build/bin/mm-lean4" ./run-testsuite-all ./test-mm-lean4)- Reviewers read the theorem statements in
Metamath/SourceCompleteness.leanandMetamath/ParserEquivalence.lean. - Reviewers trace
parser_toDatabase_wellFormed_strong -> parser_frameDerivable_to_operational -> frameDerivable_to_proofValid. - Reviewers run
lake buildand the full test suite.
lake build- Lake executables are
mm-lean4andvalidateDB. - The executable build target is
lake build mm-lean4 validateDB.