feat(provers): add Deno-native theorem prover integration#4
Merged
Conversation
Implement comprehensive prover integration system using Deno (no npm): Clients: - SystemOnTPTP: 40+ provers (Vampire, E, Z3, CVC5, SPASS, etc.) - Metamath: proof verification and theorem exploration - Z3 WASM: local SMT solving via WebAssembly - Wolfram Alpha: natural language proofs (2000 free calls/month) - LeanTool: Lean 4 via OpenAI-compatible API - Unified: aggregates all backends with strategy selection Runner: - Continuous daemon for day/night proof checking - CLI with health check, single solve, batch processing - Queue management with priority and retry logic - Persistent result storage Enforcement: - npm ban script and pre-commit hook - deno.json with strict configuration - NPM_BANNED.md documentation All imports use https:// URLs or npm: specifiers (Deno-native).
hyperpolymath
added a commit
that referenced
this pull request
Apr 20, 2026
Implement comprehensive prover integration system using Deno (no npm): Clients: - SystemOnTPTP: 40+ provers (Vampire, E, Z3, CVC5, SPASS, etc.) - Metamath: proof verification and theorem exploration - Z3 WASM: local SMT solving via WebAssembly - Wolfram Alpha: natural language proofs (2000 free calls/month) - LeanTool: Lean 4 via OpenAI-compatible API - Unified: aggregates all backends with strategy selection Runner: - Continuous daemon for day/night proof checking - CLI with health check, single solve, batch processing - Queue management with priority and retry logic - Persistent result storage Enforcement: - npm ban script and pre-commit hook - deno.json with strict configuration - NPM_BANNED.md documentation All imports use https:// URLs or npm: specifiers (Deno-native). Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
pushed a commit
that referenced
this pull request
May 26, 2026
Closes Audit-A new-doc gap #4: no single doc enumerated the env vars the system reads. This file lists ECHIDNA_ML_API_URL, VERISIM_URL, ECHIDNA_MAX_PROOF_STATES, ECHIDNA_NUM_EPOCHS, ECHIDNA_NUM_NEGATIVES, ECHIDNA_MODELS_DIR, FARM_DISPATCH_TOKEN, VERISIMDB_PAT, deprecated VERISIMDB_URL, and notes the Cargo features that gate functionality (verisim, chapel). https://claude.ai/code/session_01YPqu7gti4azBach6ZvpRFJ
3 tasks
hyperpolymath
added a commit
that referenced
this pull request
Jun 4, 2026
…arding (closes B7) (#218) ## Summary This PR **corrects a factual error** in the 2026-06-03 _"what stops echidna from running proof work across the estate"_ audit. The B7 entry said: > _HP type-checker ecosystem (13 provers) corpus-only — Rust adapters not scaffolded in `src/rust/provers/`._ That is wrong. The backends exist and are wired: | File | Lines | What's there | |---|---|---| | `src/rust/provers/hp_ecosystem.rs` | 50-153 | `HPEcosystemBackend`: full `ProverBackend` impl, parse_file / parse_string / apply_tactic / verify_proof | | `src/rust/provers/mod.rs` | 1774-1824 | `ProverFactory::create` routes TypeLL + KatagoriaVerifier through `HPEcosystemBackend`, 39 other `*TypeChecker` variants through `TypedWasmBackend::for_kind` | | `tests/common/mod.rs` | 114, 185, 245 | HP-ecosystem dispatch already special-cased in the smoke harness | | `tests/gnn_augment_integration.rs` | 545 | `test_hp_ecosystem_gnn_wires_top_premise` covers GNN wiring | ## What's actually outstanding The audit's underlying intuition (estate proof work won't run end-to-end on these provers) is correct, but the gap is downstream of the scaffold: 1. **Upstream binaries are not packaged** — `typell`, `katagoria`, `tropical-type-check` aren't in any Containerfile or `manifests/live-provers.scm`. CI runs get "binary not found" rather than verify results. 2. **No smoke fixtures** for the three Tier-8-canonical provers (Echo, Tropical, Kategoria). _Added here._ 3. **No documented onboarding** for new HP disciplines, even though the pattern is mechanical (~4 files). _Added here._ ## What this PR delivers - `docs/handover/B7-AUDIT-CORRECTION.md` — correction memo with file:line evidence. - `tests/fixtures/hp/echo_trivial.tll` — discipline `echo`, identity goal. - `tests/fixtures/hp/tropical_trivial.tll` — discipline `tropical`, zero-cost identity. - `tests/fixtures/hp/katagoria_trivial.k` — discipline `verify`, identity isomorphism. - `docs/HP-BACKEND-ONBOARDING.md` — step-by-step for adding a new HP discipline, with line refs into the 4 files an author must touch. ## What this PR does NOT do - Does not add stub backends (they exist; stubbing would regress). - Does not package the upstream binaries (deferred to D18 / L3 gate path). - Does not extract per-discipline GNN training data (deferred — F26 TypeDiscipline Phase-2). ## Test plan - [x] Three smoke fixtures parse as valid `#discipline:`-tagged source. - [x] No code changes (docs + fixtures only), so no compile/test regression possible. - [ ] Owner reviews the correction and confirms B7 is now correctly characterised. ## Estate context This PR is **#4 of 5** in the C12/C14/C15/B7/D18 critical-blocker pass. - C12 PR (echidnabot manifest): hyperpolymath/echidnabot#84 - C14 PR (cross-repo proof DAG design): #217 - C15 PR (gitbot-fleet hypatia wiring): hyperpolymath/gitbot-fleet#257 - D18 PR (L3 gate checklist): queued 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implement comprehensive prover integration system using Deno (no npm):
Clients:
Runner:
Enforcement:
All imports use https:// URLs or npm: specifiers (Deno-native).