Repository navigation
feat(schema): add literature-lineage, idea-attribution, and prior-art records #7
Description
Goal
Extend MathCorpus so formal correctness, source provenance, and intellectual lineage are separately auditable.
Packet-level source provenance is not enough for AI-assisted proofs. The corpus must record which papers, theorem statements, constructions, and proof strategies were available to the model, which were discovered only during post-hoc review, and how each relates to the final proof.
Scope
Add versioned MCIP-compatible child schemas for:
LiteratureSourceRetrievedPassageExternalClaimIdeaAttributionPriorArtMatchCitationReviewContributionStatement
Records should support:
- bibliographic metadata and stable identifiers
- source and passage hashes
- model-visible versus post-hoc sources
- links from sources to proof variants, proof-profile features, theorem dependencies, and research objects
- attribution statuses such as
directly_used,likely_influential,background_only,independent_rediscovery,uncertain, andnot_used - reviewer confidence, notes, and conflicting reviews
Acceptance criteria
- Literature lineage is represented as child evidence and never changes kernel-verification status.
- Every attribution claim is bound to packet, statement, proof variant, and source hashes.
- The schema distinguishes a source citation from a claim that the source influenced the proof.
- Model-visible literature and post-hoc prior-art findings cannot be conflated.
- Multiple or disputed attribution reviews can coexist without silently overwriting one another.
- Public exports can redact passages while retaining citation metadata and hashes.
- CDC is added as a fixture with prior Fano-flow work and the formal verification contribution identified separately.
- Validation rejects dangling source, claim, proof, or packet references.
Activity
Mnehmos commentedon Jul 12, 2026
Implemented (local commit
ae51810, stacked on928b2be/ed2e1a7/b3bfa63/bcdb683/8c74201/7f1ac10— not yet pushed, see notes on #1-#6).Important note on the fixture requirement first: the acceptance criteria name "CDC" with "prior Fano-flow work" as the fixture target. I searched this repo thoroughly (packets/, lean/, docs/, agents/) and neither "CDC" nor "Fano" appears anywhere — this doesn't correspond to any content in this corpus. Rather than fabricate that scenario, I substituted
packets/frontier/formal_conjectures/union_closed_sharpness.v1.json— a real packet whose own pre-existing notes already document genuine literature provenance (a FormalConjectures Lean source, Wikipedia background, and a citation to Yu 2023's improved general-case bound as distinct prior art). If "CDC"/Fano-flow work exists in a different repo or is planned future content, this issue's fixture requirement should be re-scoped to that when it lands here — I didn't want to invent placeholder content that would misrepresent this corpus's actual state.7 new MCIP schemas (
schema/mcip/v1/) beyond #1's original 10:LiteratureSource,RetrievedPassage,ExternalClaim,IdeaAttribution,PriorArtMatch,CitationReview,ContributionStatement. Matching packet-embedded shapes:idea_attributions[],prior_art_matches[],citation_reviews[],contribution_statements[].LiteratureSource/RetrievedPassage/ExternalClaimlive in a new sharedliterature_sources/catalog (same pattern asrestriction_profiles/from feat(schema): add proof profiles, restriction profiles, and proof variants #2) — a source cited by multiple packets is stored once.tools/stamp_literature_sources.pystampsrecord_hash.IdeaAttribution.visibility(model_visible/post_hoc) plusPriorArtMatchbeing a structurally distinct record type — no shared visibility field, since a prior-art match is post-hoc by construction — is the mechanism, not just a convention.formal_statement_sha256+source_sha256_pin(hash-pins the catalog entry, exactly likeproof_variants[].restriction_profile_sha256).ExternalClaimrecords what a source asserts;IdeaAttributionseparately claims whether/how it influenced a proof.citation_reviews[]is an array;supersedespoints backward to an earlier review it updates rather than editing history away.RetrievedPassage.passage_redacted+ nullablepassage_textalongside requiredpassage_sha256;policy.check_literature_source_catalogrejects a redacted passage that still carries its text.contribution_classvocabulary defined here (new_proof,independent_rediscovery,formalization,verification,reconstruction,adaptation,literature_derived_synthesis) for feat(policy): require contribution, citation, and novelty review for open-problem exports #8's publication policy to require.policy.check_literature_lineage(per-packet) +check_literature_source_refs(corpus-wide catalog resolution, stale hash-pin detection).Real, honestly-graded fixture:
union_closed_sharpness.v1gets 2idea_attributions(the FormalConjectures source,directly_used/model_visible; Wikipedia,background_only), 1prior_art_match(Yu 2023,related_technique— explicitly a different, narrower claim than this packet's sharpness-of-1/2 result, not a duplicate), 1citation_review(endorsed, confidence 0.8), and 1contribution_statement(contribution_class: "adaptation"— it's a transported/adapted proof, not anew_proof). The Yu 2023 catalog entry is explicitly marked bibliographically unverified (its title/author come from the packet's own pre-existing notes text, not an independently checked bibliography) — this corpus's honesty standard extends to not overclaiming citation precision, not just not overclaiming proof results.Cross-cutting fix found via testing:
schema/mcip/v1/_defs.schema.jsonhad an invalidenvelope_requiredkey — a plain array masquerading as a subschema, failing strictcheck_schema. Latent since #1, never triggered before because nothing previously validated every schema file in the registry including_defs.schema.jsonitself. Removed (zero references anywhere).10 failure modes smoke-tested directly. Full corpus (357 packets) + full CI-equivalent pipeline + issue #6 tooling (importer dry-run, backfill report) verified locally, 0 errors.
Tracked in
agents/github_issues/DONE.md,FEATURES.md,HANDOFF.md.feat(schema): add literature-lineage, idea-attribution, and prior-art…
feat(policy): require contribution, citation, and novelty review for …