Summary
seal() checks that lemma assumptions do not contradict axioms, but does not require the axiom set to justify those assumptions. This creates a gap in the explicit-assumptions model that is central to symproof's value proposition.
Problem
verify_lemma() actively uses Lemma.assumptions in two ways:
- Substitutes assumption-enhanced symbols into expressions (line 235–236)
- Passes assumptions as Q-context to
sympy.ask() for QUERY lemmas (lines 350–351)
seal() runs _check_assumptions_consistent() (bundle.py lines 32–63) which only checks that axiom expressions are not provably False under the lemma assumptions. Indeterminate results are allowed (line 44: "Only proven contradictions are rejected").
The load-bearing audit (_audit_load_bearing) catches Symbol constructor assumptions (e.g., Symbol("x", positive=True)) that affect verification but lack axiom backing. However, dict-based assumptions passed via Lemma.assumptions — which feed directly into sympy.ask() contexts — are not subject to load-bearing analysis.
A proof author can introduce {"x": {"positive": True}} in a lemma's assumptions dict without any axiom declaring x > 0. The proof will seal successfully as long as the assumption doesn't contradict existing axioms.
Suggested fix
Extend _audit_load_bearing (or add a parallel check) to also cover dict-based Q-context assumptions on QUERY lemmas, requiring that each such assumption is backed by an axiom in the set.
Files
symproof/verification.py — verify_lemma(), _build_assumption_subs(), _build_q_context()symproof/bundle.py — seal(), _check_assumptions_consistent(), _audit_load_bearing()
Summary
seal()checks that lemma assumptions do not contradict axioms, but does not require the axiom set to justify those assumptions. This creates a gap in the explicit-assumptions model that is central to symproof's value proposition.Problem
verify_lemma()actively usesLemma.assumptionsin two ways:sympy.ask()for QUERY lemmas (lines 350–351)seal()runs_check_assumptions_consistent()(bundle.py lines 32–63) which only checks that axiom expressions are not provably False under the lemma assumptions. Indeterminate results are allowed (line 44: "Only proven contradictions are rejected").The load-bearing audit (
_audit_load_bearing) catches Symbol constructor assumptions (e.g.,Symbol("x", positive=True)) that affect verification but lack axiom backing. However, dict-based assumptions passed viaLemma.assumptions— which feed directly intosympy.ask()contexts — are not subject to load-bearing analysis.A proof author can introduce
{"x": {"positive": True}}in a lemma's assumptions dict without any axiom declaringx > 0. The proof will seal successfully as long as the assumption doesn't contradict existing axioms.Suggested fix
Extend
_audit_load_bearing(or add a parallel check) to also cover dict-based Q-context assumptions on QUERY lemmas, requiring that each such assumption is backed by an axiom in the set.Files
symproof/verification.py—verify_lemma(),_build_assumption_subs(),_build_q_context()symproof/bundle.py—seal(),_check_assumptions_consistent(),_audit_load_bearing()