Popular repositories Loading
-
BusyBeaver-1-
BusyBeaver-1- PublicFully verified Coq proof for the one-state Busy Beaver machine — a minimal example of formal halting verification.
Rocq Prover
-
mini_Collatz_demo-
mini_Collatz_demo- PublicMinimal Coq formalization of Collatz iteration with proofs and computations (n27 ->1)
-
-
-
MinimalSIGDemo
MinimalSIGDemo PublicCoq & Lean4 minimal formal demo for a Collatz-style iterator: gate reachability + unique gate index
Lean
-
Something went wrong, please refresh the page to try again.
If the problem persists, check the GitHub status page or contact support.
If the problem persists, check the GitHub status page or contact support.