Pinned Loading

1. mit-plv/fiat-crypto mit-plv/fiat-crypto Public

   Cryptographic Primitive Code Generation by Fiat

   Rocq Prover 776 155

2. guarantees-based-mechanistic-interpretability guarantees-based-mechanistic-interpretability Public

   Jupyter Notebook 16 2

3. HoTT/Coq-HoTT HoTT/Coq-HoTT Public

   A Coq library for Homotopy Type Theory

   Rocq Prover 1.3k 197

4. coq-tools coq-tools Public

   Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

   Python 43 9

5. lob lob Public

   Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/). Write-up at https://github.com/JasonGross/lob-paper

   Agda 24 2

6. rocq-prover/rocq rocq-prover/rocq Public

   The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

   OCaml 5.2k 693