Summary
INFERENCE lemmas in symproof/verification.py (lines 407–430) are verified only structurally — the verifier checks that depends_on is non-empty and rule is non-empty, but performs no mechanical verification that the inference follows from its premises.
Problem
The current checks (lines 407–421):
depends_on must be non-emptyrule must be non-empty
What is not checked:
- Whether lemmas named in
depends_on actually exist in the proof script
- Whether the named
rule is a recognized logical principle
- Whether the conclusion (
lemma.expr) actually follows from the cited dependencies
This means any claim can pass verification by citing an arbitrary rule name and dependency name. While the docs are honest about this limitation, sealed proof bundles do not clearly flag which steps are human-asserted vs. machine-checked.
Suggested improvements
- Minimum: Validate that all
depends_on names resolve to earlier lemmas in the script
- Medium: Add an advisory to sealed bundles explicitly listing INFERENCE lemmas as human-asserted steps
- Long-term: Consider a registry of known inference rules with mechanized checking
Files
symproof/verification.py:407-430
Summary
INFERENCE lemmas in
symproof/verification.py(lines 407–430) are verified only structurally — the verifier checks thatdepends_onis non-empty andruleis non-empty, but performs no mechanical verification that the inference follows from its premises.Problem
The current checks (lines 407–421):
depends_onmust be non-emptyrulemust be non-emptyWhat is not checked:
depends_onactually exist in the proof scriptruleis a recognized logical principlelemma.expr) actually follows from the cited dependenciesThis means any claim can pass verification by citing an arbitrary rule name and dependency name. While the docs are honest about this limitation, sealed proof bundles do not clearly flag which steps are human-asserted vs. machine-checked.
Suggested improvements
depends_onnames resolve to earlier lemmas in the scriptFiles
symproof/verification.py:407-430