proof-certificates

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.

Width-independent proof certificates for KnownBits and word programs, with research tools and a Lean 4 formalization pilot.

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.

Exact proof objects and standalone verification for weighted-sum supportability and unsupportedness in finite multi-objective optimisation.

A length-22 permutation that three stacks in series cannot sort, with a machine-checkable DRAT certificate. Superseded by Pantone-Vatter (2026).

Exact certificates for a Schmidt-number-two bound, an explicit qutrit violation, and supporting two-sided partial-locality geometry.

A benchmark for chess mate-solving engines: every claimed mate verified by proof certificate, paired comparisons, and positions no engine has seen.

Paused OPN research program: scoped results, exact certificates, countermodels, reports, and open frontiers. No OPN proof is claimed.

Unresolved Erdos 2^k 3^l m + 1 cover search with exact finite certificates and independent verifiers