Pinned Loading

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

   Cryptographic Primitive Code Generation by Fiat

   Rocq Prover 812 167

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

   Jupyter Notebook 18 2

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

   A Coq library for Homotopy Type Theory

   Rocq Prover 1.4k 201

4. coq-tools coq-tools Public

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

   Python 46 9

5. lob lob Public

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

   Agda 26 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.4k 721