ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance. Neurosymbolic theorem proving with 30 prover backends
-
Updated
Aug 24, 2026 - Rust
ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance. Neurosymbolic theorem proving with 30 prover backends
Open computational evidence infrastructure for Lean - Turns external solver results into Lean-checked evidence through explicit contracts, replayable bundles, and untrusted computer-algebra adapters.
Executable certificate framework for a proof candidate of Graham’s rearrangement conjecture / Erdős #475, with local branch checkers and reproducible audit scripts.
Exact proof objects and standalone verification for weighted-sum supportability and unsupportedness in finite multi-objective optimisation.
Paused OPN research program: scoped results, exact certificates, countermodels, reports, and open frontiers. No OPN proof is claimed.
Independent audit and finite-obstruction research for Seymour's Second Neighborhood Conjecture at minimum outdegree eight
Unresolved Erdos 2^k 3^l m + 1 cover search with exact finite certificates and independent verifiers
Add a description, image, and links to the proof-certificates topic page so that developers can more easily learn about it.
To associate your repository with the proof-certificates topic, visit your repo's landing page and select "manage topics."