Repository navigation
feat(schema): add proof profiles, restriction profiles, and proof variants #2
Description
Problem
Packets currently record tactics and basic metrics but cannot distinguish theorem lookup, normalization, arithmetic automation, induction, witness construction, case analysis, or multi-lemma composition. They also represent only one canonical proof and cannot encode benchmark restrictions.
Scope
Extend MathCorpus with child records for:
ProofProfileProofVariantRestrictionProfile
Suggested profile fields include primary and secondary proof classes, automation level, retrieval depth, planning depth, branch count, witness invention, induction, contradiction, case analysis, and dependency composition.
Proof variants should support canonical, shortest, pedagogical, restricted, interactive, and alternate-model styles without mutating the immutable packet identity.
Restriction profiles should support forbidden tactics, allowed tactics, allowed dependency sets, maximum tactic or dependency counts, and requirements for explicit intermediate claims.
Acceptance criteria
- Packet schema can reference zero or more versioned child proof variants.
- Proof-profile vocabulary is documented and validated.
- Restriction profiles are hash-pinned and reusable across packets.
- Canonical proof identity remains stable when variants are added.
- At least five elementary algebra packets are migrated as fixtures.
- Validation rejects a variant whose statement, packet, environment, or proof hash does not match its parent evidence.
Activity
Mnehmos commentedon Jul 12, 2026
Implemented (local commit
8c74201, stacked on7f1ac10from #1 — not yet pushed, see note on #1):packet.schema.jsongainsproof_variants[]($defs.proof_variant/$defs.proof_profile), mirroring MCIP'sProofVariant/ProofProfileshapes from feat(schema): define MathCorpus Interchange Protocol v1 for Proof Search enrichment #1. Styles:canonical,shortest,pedagogical,restricted,interactive,alternate_model.proof_profilecarries primary/secondary proof class (theorem_lookup,normalization,arithmetic_automation,induction,witness_construction,case_analysis,multi_lemma_composition), automation level, retrieval/planning depth, branch count, and witness/induction/contradiction/case-analysis flags.policy.check_proof_variantsrejects a variant whose statement or environment hash disagrees with its parent packet, and (forcanonical-styled variants specifically) whoseproof_body_sha256disagrees with the packet's own recorded proof hash. Smoke-tested directly.restriction_profiles/catalog reusesschema/mcip/v1/restriction_profile.schema.jsondirectly (no duplicate schema) so profiles live once and are referenced by(restriction_profile_id, restriction_profile_sha256)from any packet'sproof_variants.tools/stamp_restriction_profiles.pystampsrecord_hash;policy.check_restriction_profile_refsrejects a dangling id or a stale hash pin.tools/validate_packets.pynow validates the catalog automatically — no CI change needed beyond the existing invocation.add_assoc,add_comm,add_left_comm,add_mul,add_zeroeach get acanonicalvariant;add_assocandadd_muladditionally get arestrictedvariant pinned to a sharedno_ring_automationprofile — verified true by reading their actual.leanproof bodies (neither usesring/ring_nf/noncomm_ring), not fabricated.Tracked in
agents/github_issues/DONE.md,FEATURES.md,HANDOFF.md.feat(schema): add proof profiles, restriction profiles, proof variants (
feat(import): add MCIP importer, packet enrichment workflow, and back…
feat(schema): add literature-lineage, idea-attribution, and prior-art…