elliotglazer/k230-rocq
Axiom-free Rocq verification that a certain 230-state Turing machine (K230) halts iff ZFC is inconsistent, and a classical Rocq verification that PA proves "K230 halts iff NOT Con(ZFC)".
GitHub repository with 10 stars and 0 forks.
Language: Rocq Prover