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.
Exact certificates for a Schmidt-number-two bound, an explicit qutrit violation, and supporting two-sided partial-locality geometry.
A length-22 permutation that three stacks in series cannot sort, with a machine-checkable DRAT certificate. Superseded by Pantone-Vatter (2026).
Independent audit and finite-obstruction research for Seymour's Second Neighborhood Conjecture at minimum outdegree eight
Certified proof frontier for K_2(11,3): 112/150 normalized and 324/350 selected branch closures; the exact value remains open.
Unresolved Erdos 2^k 3^l m + 1 cover search with exact finite certificates and independent verifiers
To associate your repository with the proof-certificates topic, visit your repo's landing page and select "manage topics."