Repository navigation

feat(corpus): resolved & expanded training corpus (700K+ proofs) - #25

Merged

hyperpolymath merged 449 commits into

mainfrom

claude/expand-vocabulary-corpus-1SFwy

Apr 20, 2026

Merged

feat(corpus): resolved & expanded training corpus (700K+ proofs)#25
hyperpolymath merged 449 commits into
mainfrom
claude/expand-vocabulary-corpus-1SFwy

This pull request is big! We're only showing the most recent 250 commits

Commits on Mar 16, 2026
- migrate: .scm → .a2ml state files in .machine_readable/
  
  hyperpolymath
  and
  claude
  committed
  12b6437
- ci: deploy missing standard workflows (2 added)
  
  hyperpolymath
  and
  claude
  committed
  25cae21
- chore: restructure 6a2ml files into .machine_readable/6a2/
  hyperpolymath
  committed
  4aa717f
- chore: add SPDX headers to source files
  hyperpolymath
  committed
  6041c4a
- chore: clean up legacy Trustfile.hs, example Trustfiles, and AI.djot files
  
  hyperpolymath
  and
  claude
  committed
  167292f
- chore: restructure nested 6a2ml files into .machine_readable/6a2/
  hyperpolymath
  committed
  1277311
- feat: add CLADE.a2ml — clade taxonomy declaration
  
  hyperpolymath
  and
  claude
  committed
  78a38fa
- chore: update manifest paths to .machine_readable/6a2/
  hyperpolymath
  committed
  aae7907
- chore: SHA-pin GitHub Actions for supply chain security
  
  hyperpolymath
  and
  claude
  committed
  9e8bfeb
- chore: add #![forbid(unsafe_code)] to safe Rust crates
  
  hyperpolymath
  and
  claude
  committed
  f40d67a
Commits on Mar 17, 2026
Commits on Mar 18, 2026
Commits on Mar 20, 2026
- chore(ci): maximize ci/cd values via dependabot and permissions
  hyperpolymath
  committed
  1c8f877
- fix(ci): Resolve workflow-linter self-matching and metadata issues
  hyperpolymath
  committed
  cf8468c
- chore: CI/CD permissions refinement, FFI wrappers, corpus expansion tooling
  
  hyperpolymath
  and
  claude
  committed
  ae9844b
- chore: CI/CD permissions refinement, FFI wrappers, corpus expansion tooling
  
  hyperpolymath
  and
  claude
  committed
  1183bef
- Merge remote-tracking branch 'gitlab/main'
  hyperpolymath
  committed
  2be1e5c
- feat(chapel): Enable Chapel accelerator build integration
  
  hyperpolymath
  and
  claude
  committed
  7be0efb
- feat(llm): Add frontier LLM advisor via BoJ Server integration
  
  hyperpolymath
  and
  claude
  committed
  0994308
- Chore/cicd optimizations (#8)
  
  hyperpolymath
  and
  claude
  authored
  c55390b
- feat(verisimdb): Add 8-modality proof storage via VeriSimDB octads
  
  hyperpolymath
  and
  claude
  committed
  0b2abf6
- feat(abi-ffi): Add per-prover Idris2 ABI + Zig FFI for all 30 backends
  
  hyperpolymath
  and
  claude
  committed
  7e8a837
- feat(vql-ut): Add 10-level type-safe cross-prover query language
  
  hyperpolymath
  and
  claude
  committed
  522fedd
- fix(integration): Wire VQL-UT to VeriSimDB search + Julia embeddings
  
  hyperpolymath
  and
  claude
  committed
  2f5eb20
- feat(vql-ut): Add TypeLL pre-flight validation before query execution
  
  hyperpolymath
  and
  claude
  committed
  08fe117
Commits on Mar 21, 2026
- chore(floor-raise): add foundational tool integrations
  
  hyperpolymath
  and
  claude
  committed
  23e001a
- feat: add extraction scripts for HOL4, HOL Light, SMT-LIB, and TPTP
  
  hyperpolymath
  and
  claude
  committed
  7b7ba6f
- Merge branch 'chore/cicd-optimizations'
  hyperpolymath
  committed
  64625d9
- feat: Expand corpus to 181K+ proofs across 26 prover backends
  
  hyperpolymath
  and
  claude
  committed
  18619d1
- feat: Chapel 30-prover real dispatch, Idris2 CI, E2E smoke tests, container CI
  
  hyperpolymath
  and
  claude
  committed
  1d1f2af
- chore: eliminate all compiler warnings (0 warnings, 248 tests pass)
  
  hyperpolymath
  and
  claude
  committed
  79aa936
- chore(deps): update dependencies (fix rustls-webpki CVE)
  
  hyperpolymath
  and
  claude
  committed
  f949717
- fix: Idris2 ABI type-checks clean, ProverFactory auto-resolves executables
  
  hyperpolymath
  and
  claude
  committed
  79ac2ed
- fix(container): remove separate cargo package (included in rust on wolfi)
  
  hyperpolymath
  and
  claude
  committed
  7c5da92
- fix(container): remove standalone tar package (bundled in wolfi base)
  
  hyperpolymath
  and
  claude
  committed
  3f5c4b8
- fix(container): skip Idris2 in minimal image (no prebuilt binaries)
  
  hyperpolymath
  and
  claude
  committed
  742a04f
- fix(container): install Z3 from official release, simplify to 3 stages
  
  hyperpolymath
  and
  claude
  committed
  f79bff2
- feat(ml): wire Julia ML pipeline — data loading, training, and serving
  
  hyperpolymath
  and
  claude
  committed
  ac9d6c6
- chore(ml): fix Julia dep UUIDs, add Manifest.toml
  
  hyperpolymath
  and
  claude
  committed
  9f2bd55
- fix(ml): resolve all Julia module loading issues
  
  hyperpolymath
  and
  claude
  committed
  a819fec
- fix(ml): make training loop Zygote-differentiable and run
  
  hyperpolymath
  and
  claude
  committed
  2c4deb8
- feat(ml): training complete — MRR 0.66, Precision@10 0.30, Recall@10 0.59
  
  hyperpolymath
  and
  claude
  committed
  6caf325
- Add arXiv-style paper: Neurosymbolic Theorem Proving
  
  hyperpolymath
  and
  claude
  committed
  54e7b21
Commits on Mar 22, 2026
- chore: batch RSR compliance — SPDX headers, SHA-pin actions, forbid(unsafe_code), CODE_OF_CONDUCT, CONTRIBUTING
  
  hyperpolymath
  and
  claude
  committed
  3ca5979
- docs: add EXPLAINME.adoc — prove-it file backing README claims
  
  hyperpolymath
  and
  claude
  committed
  91db04a
- test: implement 6 agentic integration tests, fix TypedWasm match exhaustiveness
  
  hyperpolymath
  and
  claude
  committed
  0e7b857
- Add typed-wasm prover backend + property test regressions
  
  hyperpolymath
  and
  claude
  committed
  791850a
- chore: add Julia project env for test server, install Vampire 5.0.1
  
  hyperpolymath
  and
  claude
  committed
  5a1b5ac
- fix(pvs): fix PVSCaseSelection field mismatch in CASES parser
  
  hyperpolymath
  and
  claude
  committed
  ab7864c
- feat(provers): add 6 SAT/model-checker backends (NuSMV, TLC, Alloy, Prism, UPPAAL, MiniSat)
  
  hyperpolymath
  and
  claude
  committed
  8708ab2
Commits on Mar 23, 2026
- feat(provers): add 7 backends completing 48/48 target
  
  hyperpolymath
  and
  claude
  committed
  76c80b0
- chore: update STATE.a2ml date to 2026-03-23 (48 backends)
  
  hyperpolymath
  and
  claude
  committed
  a124103
- fix: compilation errors, rustfmt stable compat, cargo fmt across codebase
  
  hyperpolymath
  and
  claude
  committed
  923e6ce
Commits on Mar 24, 2026
- feat: add groove discovery endpoint for ECHIDNA
  
  hyperpolymath
  and
  claude
  committed
  e9c9790
- feat(ux): add onboarding, contractiles, and UX infrastructure
  
  hyperpolymath
  and
  claude
  committed
  4cecb4e
- chore: add Stapeln selur-compose.toml service definition
  
  hyperpolymath
  and
  claude
  committed
  a169da4
- fix: apply PORT-REGISTRY.md — neural/prover API 8081, docs-site 4070
  
  hyperpolymath
  and
  claude
  committed
  d0dc866
- fix: eliminate all clippy warnings and errors across entire codebase
  
  hyperpolymath
  and
  claude
  committed
  5610a89
- feat: add Agda meta-checker formally verifying trust pipeline
  
  hyperpolymath
  and
  claude
  committed
  51bbd5e
- feat(ffi): complete FFI bridge for all 48 prover backends
  
  hyperpolymath
  and
  claude
  committed
  a7827aa
- feat: add comprehensive Criterion benchmarks + make kind_from_u8 public
  
  hyperpolymath
  and
  claude
  committed
  bd086d3
- test: add 131 new tests across 20 modules (397→528 passing)
  
  hyperpolymath
  and
  claude
  committed
  b904d77
- chore: bump to v2.0.0, update ROADMAP and CLAUDE.md
  
  hyperpolymath
  and
  claude
  committed
  7430eb2
- Add Green Web Foundation badge (#9)
  
  hyperpolymath
  and
  claude
  authored
  0070830
Commits on Mar 28, 2026
- feat: add Groove discovery manifest
  
  hyperpolymath
  and
  claude
  committed
  f8e8eb1
- feat: add V-lang API for theorem prover client
  
  hyperpolymath
  and
  claude
  committed
  fc48e32
- chore: add UX infrastructure (quickstart, doctor, setup)
  
  hyperpolymath
  and
  claude
  committed
  02404a7
- feat: add stapeln.toml layer-based container definition\n\nConverted from existing Containerfile to stapeln format.\nIncludes Chainguard base, security hardening, SBOM generation.\n\nCo-Authored-By…
  hyperpolymath
  committed
  4da31a3
- chore: gitignore .tool-versions (asdf)
  
  hyperpolymath
  and
  claude
  committed
  710a10e
- chore: deploy UX infrastructure (contractile.just, .well-known, manifest)
  
  hyperpolymath
  and
  claude
  committed
  b567710
Commits on Mar 29, 2026
- chore: update Cargo dependencies for security
  
  hyperpolymath
  and
  claude
  committed
  7d3bd62
- chore: replace template placeholders in ROADMAP.adoc files
  
  hyperpolymath
  and
  claude
  committed
  8f6cef1
- feat: migrate all 26 corpus extraction scripts from Python to Julia
  
  hyperpolymath
  and
  claude
  committed
  23ec157
- feat: migrate all 15 TypeScript files to ReScript — zero TS remaining
  
  hyperpolymath
  and
  claude
  committed
  1c7c466
- docs: update ReScript file count (28→33) and version after TS migration
  
  hyperpolymath
  and
  claude
  committed
  a9368ea
Commits on Mar 30, 2026
- feat: 5x vocabulary expansion — 72,557 tokens across 48 provers + 10 math domains
  
  hyperpolymath
  and
  claude
  committed
  b116a3c
- feat: add GNN integration for proof search guidance (v2.1.0)
  
  hyperpolymath
  and
  claude
  committed
  54ffad8
- docs: add BibTeX bibliography for neurosymbolic theorem proving paper
  
  hyperpolymath
  and
  claude
  committed
  20a4ba2
- Remove template-only ABI files that falsely implied formal verification
  
  hyperpolymath
  and
  claude
  committed
  889b0f7
- feat: add AxiomTrackerCompleteness.agda
  
  hyperpolymath
  and
  claude
  committed
  300eff6
Commits on Mar 31, 2026
- Change Green Hosting link in README
  hyperpolymath
  authored
  510df1b
Commits on Apr 2, 2026
- Snapshot local work before sync
  hyperpolymath
  committed
  eceb2a3
- Remove template-only ABI files that falsely implied formal verification
  
  hyperpolymath
  and
  claude
  committed
  abada94
- Snapshot local work before sync
  hyperpolymath
  committed
  6608af4
Commits on Apr 3, 2026
- fix(deps): update Cargo.lock to resolve security advisories
  
  hyperpolymath
  and
  claude
  committed
  893a5c8
- feat(axioms): add really_believe_me, prim__crash (Idris2) + {!!} holes (Agda)
  
  hyperpolymath
  and
  claude
  committed
  31b71ce
Commits on Apr 4, 2026
- test: CRG C blitz — E2E, P2P, aspect, Julia, shell test coverage
  
  hyperpolymath
  and
  claude
  committed
  74f812c
- test: CRG C blitz — E2E, P2P, security, concurrency + routing benchmarks
  
  hyperpolymath
  and
  claude
  committed
  49d175e
- docs: substantive CRG C annotation (EXPLAINME.adoc)
  hyperpolymath
  committed
  5ed52c3
- fix(ci): exclude third-party HTML dirs from mixed content check
  hyperpolymath
  committed
  e09ba6e
- test: CRG B evidence — 6 external targets tested
  
  hyperpolymath
  and
  claude
  committed
  00ed2e0
- ci: deploy dogfood-gate, add Groove manifest and CRG tests
  
  hyperpolymath
  and
  claude
  committed
  592afc5
- feat: add k9iser.toml and generate K9 contracts
  
  hyperpolymath
  and
  claude
  committed
  02f23ff
- chore: add K9 Kennel-level metadata guard
  
  hyperpolymath
  and
  claude
  committed
  770ddb3
- chore: add eclexiaiser.toml energy-cost manifest
  hyperpolymath
  committed
  48a4f6d
- feat: wire conflow config validation pipeline
  hyperpolymath
  committed
  1d15844
- chore: add eclexiaiser-validate job to dogfood gate
  
  hyperpolymath
  and
  claude
  committed
  6d91448
- feat(crg): add crg-grade and crg-badge justfile recipes
  hyperpolymath
  committed
  4413f02
Commits on Apr 5, 2026
- feat(echidnabot): sync fleet additions + today's session edits
  
  hyperpolymath
  and
  claude
  committed
  161352c
- feat: close proof learning loop + scaffold-sorry policy
  
  hyperpolymath
  and
  claude
  committed
  e5f261d
- docs(proofs): record proven obligations + add VQL-UT L3/L5 lemmas
  
  hyperpolymath
  and
  claude
  committed
  6b9b823
- feat(proofs): add trust-pipeline proofs + language-provability analysis
  
  hyperpolymath
  and
  claude
  committed
  958f1b2
- chore(verification): gitignore Idris2 build artifacts
  
  hyperpolymath
  and
  claude
  committed
  e3b45f4
- docs(test-needs): file /api/verify false-positive bug
  
  hyperpolymath
  and
  claude
  committed
  a3d69ae
- feat(fly): deploy config for nesy-solver playground (Phase E3)
  
  hyperpolymath
  and
  claude
  committed
  a9e9b96
- chore(proofs): add TPTP corpus + known-good Agda witness
  
  hyperpolymath
  and
  claude
  committed
  22461a9
- feat(proofs): expand corpus for 10+ provers + fix EchidnaBuddy overclaim
  
  hyperpolymath
  and
  claude
  committed
  96dbe23
- chore(gitignore): exclude prover build artifacts from proofs/
  hyperpolymath
  committed
  b5644c6
- chore: drop Coq build artifacts from index
  hyperpolymath
  committed
  019174f
- fix(proofs): repair Agda scoping bugs + add BasicTotality.idr witness
  
  hyperpolymath
  and
  claude
  committed
  485962d
- refactor(rename): VQL → VCL + verisimdb → verisim (ecosystem consistency)
  
  hyperpolymath
  and
  claude
  committed
  6bb7846
- fix(proofs/idris2): repair 3 broken files — 5/5 now compile
  
  hyperpolymath
  and
  claude
  committed
  dcc4943
- fix(server): guard against empty-ProofState false positives in verify/prove
  
  hyperpolymath
  and
  claude
  committed
  6e3e3b3
- chore(proofs): add F* corpus (5 arithmetic lemmas)
  
  hyperpolymath
  and
  claude
  committed
  c3e9a91
- fix(provers/isabelle): de-stub parse_string + verify_proof
  
  hyperpolymath
  and
  claude
  committed
  2b36f83
- docs(changelog): consolidate 2026-04-05 Unreleased section
  
  hyperpolymath
  and
  claude
  committed
  072a41b
- docs: update CHANGELOG + STATE.a2ml for 2026-04-05 session
  
  hyperpolymath
  and
  claude
  committed
  845d80e
- fix(echidna): per-backend verify_raw + ProofComposition.agda rewrite
  
  hyperpolymath
  and
  claude
  committed
  7ea60b2
Commits on Apr 7, 2026
- fix(api): route SMT check-sat queries through raw solver eval
  hyperpolymath
  committed
  aadde78
Commits on Apr 8, 2026
- chore: automated sync of local changes
  hyperpolymath
  committed
  861374b
Commits on Apr 10, 2026
- Add Invariant Path wrapper profile for Echidna
  hyperpolymath
  committed
  cdd6bd4
- Add Just recipe for Invariant Path wrapper
  hyperpolymath
  committed
  45546e4
Commits on Apr 11, 2026
- feat(corpus): expand Isabelle/HOL corpus from 4 to 101 entries
  
  hyperpolymath
  and
  claude
  committed
  345987c
- chore(licence): clarify MPL-2.0 fallback — PMPL-1.0-or-later preferred
  
  hyperpolymath
  and
  claude
  committed
  180da4d
- feat(coupling): wire echidnabot → VeriSimDB + Julia retrain pipeline
  
  hyperpolymath
  and
  claude
  committed
  413a6a9
- fix(fly): cold-start hardening — 90s grace, HTTP health check, curl
  
  hyperpolymath
  and
  claude
  committed
  81ab217
- feat(echidnabot+retrain): wire VeriSimDB dogfood loop end-to-end
  
  hyperpolymath
  and
  claude
  committed
  9dab534
- chore(6a2): update echidnabot STATE + fix Intentfile copy-paste
  
  hyperpolymath
  and
  claude
  committed
  3fece4e
- docs(machine-readable): update 6a2 for 2026-04-11 Fly cold-start hardening session
  
  hyperpolymath
  and
  claude
  committed
  bf5ad37
- feat(v2.2): epistemic hardening — Z3 easy fixes, integration wiring, roadmap
  
  hyperpolymath
  and
  claude
  committed
  0d39ea1
- chore(models): commit retrain metadata from 2026-04-11 VeriSimDB loop
  
  hyperpolymath
  and
  claude
  committed
  6323903
- chore(6a2): commit pre-existing 6a2 sweep for echidnabot, HOL-o-extension, echidna-playground
  
  hyperpolymath
  and
  claude
  committed
  e847c86
- chore(6a2): migrate bot_directives to A2ML, remove deprecated .scm metadata files
  
  hyperpolymath
  and
  claude
  committed
  fefef25
- chore(contractiles): migrate to .machine_readable/contractiles/ (canonical)
  
  hyperpolymath
  and
  claude
  committed
  8f403a9
- proof: E4 trust level soundness (Idris2 complement to Lean4 ConfidenceLattice)
  
  hyperpolymath
  and
  claude
  committed
  7118b63
Commits on Apr 12, 2026
- feat(echidnabot): harden webhook signing + prover-unavailable distinction
  
  hyperpolymath
  and
  claude
  committed
  25af504
- chore(ui): migrate Justfile to deno task + update ReScript UI layer
  
  hyperpolymath
  and
  claude
  committed
  6a62b9f
Commits on Apr 15, 2026
- chore: M5 CI/Workflow Sweep - add blockers and contractile.just
  hyperpolymath
  committed
  30f53f7
- chore: track (empty) deno.lock for M5 sweep
  hyperpolymath
  committed
  1124a51
Commits on Apr 16, 2026
- chore: M5 CI/Workflow Sweep - final synchronisation
  hyperpolymath
  committed
  9f06c46
Commits on Apr 17, 2026
- chore: update LICENSE to PMPL-1.0-or-later with MPL-2.0 fallback
  hyperpolymath
  committed
  9c080c7
- chore: sync chore drift (docs, workflows, gitignore, a2ml)
  
  hyperpolymath
  and
  claude
  committed
  1664b4e
- chore: fix stale absolute-path references (estate move 2026-04-17)
  
  hyperpolymath
  and
  claude
  committed
  1f5ca86
- feat(corpus): add typechecker-ecosystem prover families + vocabulary
  
  hyperpolymath
  and
  claude
  committed
  94e2585
- feat(vocab): curated CANON seed wired into training tokenizer
  
  hyperpolymath
  and
  claude
  committed
  3cd7195
- feat(corpus): Agda extractor — 1 → 5,529 proofs from agda-stdlib
  
  hyperpolymath
  and
  claude
  committed
  0252d61
- feat(corpus): AFP extractor — Isabelle 98 → 20,584 proofs
  
  hyperpolymath
  and
  claude
  committed
  993d1c7
- corpus: fold Agda + AFP into merge_corpus, regenerate UNIFIED stats
  
  hyperpolymath
  and
  claude
  committed
  5de685e
- feat(vocab): corpus-mined tokens → CANON 8,887 → 114,983 (12.9×)
  
  hyperpolymath
  and
  claude
  committed
  573eecf
- feat(vocab): cap CANON at ~100K tokens via MAX_MINED
  
  hyperpolymath
  and
  claude
  committed
  ffe2a56
- corpus: AFP → 50K, broader Agda extraction, rebalance
  
  hyperpolymath
  and
  claude
  committed
  1753cd0
- feat(metrics): scaffold eight-axis corpus metrics suite with VeriSim sink
  
  hyperpolymath
  and
  claude
  committed
  9ccccac
- fix(metrics): wire TPTP a2ml corpus into metric loader
  
  hyperpolymath
  and
  claude
  committed
  5f4947d
- feat(metrics): floor-progress ledger with per-5 milestone banners
  
  hyperpolymath
  and
  claude
  committed
  a73b3b4
- feat(provers): onboard HP type-checker ecosystem as 13 new ProverKinds
  
  hyperpolymath
  and
  claude
  committed
  10219f5
- feat(learning): continuous self-improvement loop — MCTS + self-play + curriculum + daemon
  
  hyperpolymath
  and
  claude
  committed
  e9748ec
- feat(extract): widen HOL Light extractor — accept prove_by_refinement
  
  hyperpolymath
  and
  claude
  committed
  43eba6b
- feat(extract): widen HOL4 extractor — remove narrow tactic-keyword gate
  
  hyperpolymath
  and
  claude
  committed
  137ef68
- feat(extract): relax TPTP no-conjecture filter
  
  hyperpolymath
  and
  claude
  committed
  6e01cc3
- feat(extract): widen SMT-LIB extractor to full v2 logic scope
  
  hyperpolymath
  and
  claude
  committed
  7c5b6ab
- feat(disciplines): TypeDiscipline transition — 40-variant katagoria enum
  
  hyperpolymath
  and
  claude
  committed
  ec01312
- fix(echidna): resolve dropped ProverOutcome-taxonomy tech debt blocking full cargo check/test
  
  hyperpolymath
  and
  claude
  committed
  1021c8f
Commits on Apr 18, 2026
- docs: land ECHIDNA × VeriSim triangulation plan + Phase 1 results
  
  hyperpolymath
  and
  claude
  committed
  1a0c4a7
- feat(disciplines): Axis-1-first reframe + provers_serving() cross-index
  
  hyperpolymath
  and
  claude
  committed
  a5b1047
- feat(provers): add ProverKind::Lean3 — Three-Layer Completeness first-step
  
  hyperpolymath
  and
  claude
  committed
  cc69958
- feat(abella+nominal): add Abella prover + Nominal discipline (41st)
  
  hyperpolymath
  and
  claude
  committed
  90fd9a8
- fix(extract): rewrite Coq/CoqGym extractor — 14 → 85,190 proofs (echidna#13)
  
  hyperpolymath
  and
  claude
  committed
  2ac645d
- feat(phase-4): Dedukti + Cameleer + ACL2s + Isabelle/ZF + Boogie
  
  hyperpolymath
  and
  claude
  committed
  7529fee
- feat(extract): widen Mizar extractor to full MML clone (echidna#14)
  
  hyperpolymath
  and
  claude
  committed
  69c2635
- feat(extract): widen Agda extractor — add cubical + unimath (echidna#17)
  
  hyperpolymath
  and
  claude
  committed
  91727f5
- chore(state): record 2026-04-18 100 K campaign session — 3 Tier A wins
  
  hyperpolymath
  and
  claude
  committed
  2bec094
- feat(corpus): Three-Layer Completeness — extractor skeletons for 18 backend-only provers
  
  hyperpolymath
  and
  claude
  committed
  3264ec9
- feat(extract): walk Flyspeck clone in HOL Light extractor (echidna#16)
  
  hyperpolymath
  and
  claude
  committed
  9aa6881
- feat(extract): widen Dafny extractor — vendor dafny-lang/dafny tests (echidna#16)
  
  hyperpolymath
  and
  claude
  committed
  e3d5a0e
- feat(extract): walk CakeML clone in HOL4 extractor
  
  hyperpolymath
  and
  claude
  committed
  91a5d96
- feat(phase-4-variety): Naproche + Matita + Arend + Athena + λProlog + Mercury + Nitpick + Nunchaku
  
  hyperpolymath
  and
  claude
  committed
  60e27f8
- feat(extract): vendor + widen Tier B provers (Why3, PVS, F*, Idris2)
  
  hyperpolymath
  and
  claude
  committed
  d17ab3d
- chore(state): record 2026-04-18 100 K campaign session rollup
  
  hyperpolymath
  and
  claude
  committed
  28cb74f
- feat(extract): vendor ACL2 Community Books + MiniZinc benchmarks
  
  hyperpolymath
  and
  claude
  committed
  618d6b9
- chore(state): record Tier C vendoring + ACL2/MiniZinc boost
  
  hyperpolymath
  and
  claude
  committed
  e535f3a
- chore(state): Tier C wave 2 — Spin / SeaHorn / KeY / Prism unlocked
  
  hyperpolymath
  and
  claude
  committed
  9e9ffd6
- chore(state): Tier C wave 3 — dReal / Cameleer / Abella / Dedukti / Arend unlocked
  
  hyperpolymath
  and
  claude
  committed
  1705563
- chore(state): 2026-04-18 session rollup — 27 provers, ~442 K records
  
  hyperpolymath
  and
  claude
  committed
  1fc0937
- feat(extract): add OpenTheory extractor — pre-aligned cross-prover triangulation corpus
  
  hyperpolymath
  and
  claude
  committed
  3dbe8cf
- feat(extract): widen Boogie/SeaHorn/Dedukti — push past 2K ML threshold
  
  hyperpolymath
  and
  claude
  committed
  cd9e0df
- feat(extract): widen Frama-C / Abella / Matita extractors
  
  hyperpolymath
  and
  claude
  committed
  245c593
- feat(extract): unlock 7 more provers — Mercury/λProlog/Naproche/SAT trio/ABC
  
  hyperpolymath
  and
  claude
  committed
  b226668
- chore(state): full-integration push — 25 provers over 2K ML threshold
  
  hyperpolymath
  and
  claude
  committed
  c60e9df
- feat(extract): push Dedukti + λProlog past 2K ML threshold
  
  hyperpolymath
  and
  claude
  committed
  fe75f0c
- feat(extract): widen 6 extractors — 4 more provers past 2K threshold
  
  hyperpolymath
  and
  claude
  committed
  af6c64d
- feat(extract): unlock CBMC / ProVerif / TLC / Nitpick / Nunchaku from zero
  
  hyperpolymath
  and
  claude
  committed
  bd1ecd5
- feat(extract): widen ABC + Cameleer — more zero-set provers lifted
  
  hyperpolymath
  and
  claude
  committed
  949f071
- chore(state): wave 2 rollup — ~40 of 48 provers now meet ML threshold
  
  hyperpolymath
  and
  claude
  committed
  72ace87
- feat(extract): unlock UPPAAL / Athena / TypedWasm + scale synthetic tail
  
  hyperpolymath
  and
  claude
  committed
  c9a8289
- chore(state): full-integration complete — all 48 provers meet ML bar
  
  hyperpolymath
  and
  claude
  committed
  2fa2fd3
- feat(extract): Phase B — vendor doc's variety shortlist
  
  hyperpolymath
  and
  claude
  committed
  cf620db
- fix(extract): rewrite Metamath extractor to handle multi-line + walk all databases
  
  hyperpolymath
  and
  claude
  committed
  4f76db4
- feat(extract): push Coq past 100K — add MathComp-analysis + InteractionTrees + category-theory
  
  hyperpolymath
  and
  claude
  committed
  c51fb02
- feat(extract): widen Mizar extractor — definitions/schemes/notations/reserves
  
  hyperpolymath
  and
  claude
  committed
  2aec4ad
- chore(state): Phase A+B+C rollup — 4 provers past 100K bar
  
  hyperpolymath
  and
  claude
  committed
  f5588a9
- feat(extract): Phase A push — Lean 3 + Mathcomp toward 100K
  
  hyperpolymath
  and
  claude
  committed
  3014eb2
- feat(extract): Agda literate .lagda.md preprocessor
  
  hyperpolymath
  and
  claude
  committed
  a769195
- feat(extract): TPTP/SMT-LIB full-share + Why3 widening
  
  hyperpolymath
  and
  claude
  committed
  20189e9
- feat(extract): MiniZinc full-share + gitignore TPTP output
  
  hyperpolymath
  and
  claude
  committed
  53f0fdf
- feat(corpus): add ~60 training-data outputs + balance scripts + floor tracker
  
  hyperpolymath
  and
  claude
  committed
  9408dc4
- chore(state): session close — Step 3 corpus push wrap-up
  
  hyperpolymath
  and
  claude
  committed
  c430305
- feat(extract): AFP per-article cap 70 → 200 (50K → 106K)
  
  hyperpolymath
  and
  claude
  committed
  8a02395
- feat(extract): Agda cleared 50K target (#18); Dafny widened (+4 corpora)
  
  hyperpolymath
  and
  claude
  committed
  a6a6e8d
- feat(extract): close #16 Dafny 100K + widen λProlog / Mercury / HOL4
  
  hyperpolymath
  and
  claude
  committed
  ec01d23
- feat(extract): HOL4 / HOL Light / Why3 — +3 more past or near 100K
  
  hyperpolymath
  and
  claude
  committed
  0a6819f
- feat(extract): F* — walk HACL* (LowStar crypto corpus)
  
  hyperpolymath
  and
  claude
  committed
  6db9671
- feat(extract): add Rocq to Coq-family walk (108K → 112K)
  
  hyperpolymath
  and
  claude
  committed
  79fed35
- fix(extract): SMT-LIB per-file size gate + try/catch
  
  hyperpolymath
  and
  claude
  committed
  cc4729a
- feat(extract): HOL4 past 100K (96K → 128K)
  
  hyperpolymath
  and
  claude
  committed
  f9af38f
- refactor(core): resolve all 14 TODOs across aspect/agent/server/integration
  
  hyperpolymath
  and
  claude
  committed
  dd0a920
- feat(outcome): re-land ProverOutcome taxonomy + restore sanity_suite
  
  hyperpolymath
  and
  claude
  committed
  e6b5852
- fix(cvc5): handle declare-fun nullary + stop greedy trim-end of assert
  
  hyperpolymath
  and
  claude
  committed
  6bbd538
- docs: refresh README/CLAUDE/EXPLAINME + STATE close-out
  
  hyperpolymath
  and
  claude
  committed
  644a7fb
- chore(state): record downstream landings — outcome taxonomy + CVC5 fix
  
  hyperpolymath
  and
  claude
  committed
  937c207
- chore(ci): fix workflow references + stale action SHAs + dependabot crates
  
  hyperpolymath
  and
  claude
  committed
  e62bf25
- chore(state): record CI hygiene close (e62bf25) — code-side failures + 6 dependabot alerts resolved
  hyperpolymath
  committed
  abc1d23
- Standardize workspace: Justfile migration and A2ML directive cleanup
  hyperpolymath
  committed
  ef8f959
- Standardize workspace: Capitalize Justfile references in scripts and docs
  hyperpolymath
  committed
  46fb5b7
- chore(contractiles): remove lust (not in 6-verb set: intend trust must bust adjust dust)
  
  hyperpolymath
  and
  claude
  committed
  4d79298
- chore: checkpoint local changes
  hyperpolymath
  committed
  eec182c
- fix(verisim): resolve 22 cargo check errors on --features verisim
  
  hyperpolymath
  and
  claude
  committed
  19f4555
- fix(ml-training): accept JSONL whitespace after colon in regex parser
  
  hyperpolymath
  and
  claude
  committed
  e93ab25
- Standardize workspace: Justfile migration and A2ML directive cleanup
  hyperpolymath
  committed
  06af550
- fix(ml-training): SimpleLogger + async flusher for background runs
  
  hyperpolymath
  and
  claude
  committed
  73dc118
- feat(ml-training): parameterise epochs + models dir via env vars
  
  hyperpolymath
  and
  claude
  committed
  27c3f25
- fix(ml-training): actually update logistic weights (was no-op)
  
  hyperpolymath
  and
  claude
  committed
  f7486fc
Commits on Apr 19, 2026
- feat(ci): L3 Wave-1 — live-prover CI scaffold (Guix-first, Nix fallback)
  
  hyperpolymath
  and
  claude
  committed
  45a7a95
- fix(chapel-ffi): bundle stubs in Zig lib so --features chapel links standalone
  
  hyperpolymath
  and
  claude
  committed
  2392923
- docs(chapel-ffi): document self-linking build + ignore regenerable outputs
  
  hyperpolymath
  and
  claude
  committed
  364c7de
- feat(ci): L3 Wave-2 — wire idris2/isabelle/dafny/fstar/tlaps + fstar+tlaps tests
  
  hyperpolymath
  and
  claude
  committed
  8bbde25
- docs(state): record L3 Wave-2 landing + Wave-3 handover hints
  
  hyperpolymath
  and
  claude
  committed
  ba7944e
- docs(handover): mirror ~/Desktop/ECHIDNA-*.md into docs/handover/
  
  hyperpolymath
  and
  claude
  committed
  3b110e7
- docs(handover): synthesis — tight TODO + STATE for L1/L2/L3
  
  hyperpolymath
  and
  claude
  committed
  9c95bd0
- feat(corpus): expand synthetic proofs for least-represented provers
  claude
  committed
  3762a58
- feat(corpus): expand synthetic proofs for 6 extract-script provers
  claude
  committed
  dd04592
Commits on Apr 20, 2026

Commits

Commits on Mar 16, 2026

Commits on Mar 17, 2026

Commits on Mar 18, 2026

Commits on Mar 20, 2026

Commits on Mar 21, 2026

Commits on Mar 22, 2026

Commits on Mar 23, 2026

Commits on Mar 24, 2026

Commits on Mar 28, 2026

Commits on Mar 29, 2026

Commits on Mar 30, 2026

Commits on Mar 31, 2026

Commits on Apr 2, 2026

Commits on Apr 3, 2026

Commits on Apr 4, 2026

Commits on Apr 5, 2026

Commits on Apr 7, 2026

Commits on Apr 8, 2026

Commits on Apr 10, 2026