Context
Part of the ECHIDNA × VeriSim triangulation plan (Phase 3). When per-prover
corpus coverage reaches ≥ 50 K records, we want to port proven theorems
across provers via Dedukti / OpenTheory. That requires a canonical
alignment schema: the same theorem, expressed in multiple prover
syntaxes, linked by a single identity.
VeriSimDB is the natural home for those alignment edges because each
project already has its own instance and the graph model is a good fit
for "same theorem, different prover" relations.
What this issue is for
Somewhere to land the RDF (or equivalent) schema design before Phase 3
triangulation starts pushing alignment edges in bulk. Nothing to
implement in ECHIDNA until the schema is proposed — ECHIDNA just needs
to know the predicate names, triple shape, and canonical-form rules.
Required schema elements (draft)
- Theorem identity: stable URI for each (prover, theorem-name) pair,
plus a canonical-form hash so renames don't fragment the graph.
- Alignment predicates: `alignsTo`, `isTranslationOf`,
`hasCanonicalForm`, `provedBy`.
- Provenance: `portedVia` → { Dedukti, OpenTheory, manual } with a
hash of the translation artefact.
- Confidence: `alignmentConfidence` ∈ [0, 1] so weak auto-ports
can coexist with hand-verified ones.
- Negative results: `cannotAlignTo` — known-impossible translations
(e.g. classical → constructive) documented so the porter doesn't
retry them.
Dependencies
- Blocks: Phase 3 cross-prover porting (ECHIDNA side).
- Depends on: nothing — schema design can start now against the current
VeriSimDB RDF core.
Links
- Plan (local, soon-to-be-archived):
~/Desktop/ECHIDNA-VERISIM-STRATEGY-2026-04-17-todo.md
(the Phase-1 widening work is landed in
hyperpolymath/echidna
commits 4a2652d..e9d3289).
- Dedukti / OpenTheory exchange layer:
hyperpolymath/echidna@src/rust/exchange/
Labels (please add if your setup permits)
- `schema`, `rdf`, `cross-prover`, `echidna`, `phase-3`
Context
Part of the ECHIDNA × VeriSim triangulation plan (Phase 3). When per-prover
corpus coverage reaches ≥ 50 K records, we want to port proven theorems
across provers via Dedukti / OpenTheory. That requires a canonical
alignment schema: the same theorem, expressed in multiple prover
syntaxes, linked by a single identity.
VeriSimDB is the natural home for those alignment edges because each
project already has its own instance and the graph model is a good fit
for "same theorem, different prover" relations.
What this issue is for
Somewhere to land the RDF (or equivalent) schema design before Phase 3
triangulation starts pushing alignment edges in bulk. Nothing to
implement in ECHIDNA until the schema is proposed — ECHIDNA just needs
to know the predicate names, triple shape, and canonical-form rules.
Required schema elements (draft)
plus a canonical-form hash so renames don't fragment the graph.
`hasCanonicalForm`, `provedBy`.
hash of the translation artefact.
can coexist with hand-verified ones.
(e.g. classical → constructive) documented so the porter doesn't
retry them.
Dependencies
VeriSimDB RDF core.
Links
~/Desktop/ECHIDNA-VERISIM-STRATEGY-2026-04-17-todo.md
(the Phase-1 widening work is landed in
hyperpolymath/echidna
commits 4a2652d..e9d3289).
hyperpolymath/echidna@src/rust/exchange/
Labels (please add if your setup permits)