Pinned Loading

1. facebookresearch/atlas-lean facebookresearch/atlas-lean Public

   ATLAS Autoformalized Textbook Library At Scale

   Lean 307 40

2. vericuda vericuda Public

   A pipeline that translates Rust GPU code into formal Coq models, as a foundation for memory model proofs

   Rocq Prover 133 3

3. gpt-erdos gpt-erdos Public

   LLM-driven proof search on Erdős problems (2 solutions accepted on erdosproblems.com)

   Lean 16 1

4. symbolic-circuit-distillation symbolic-circuit-distillation Public

   Automatically extract executable programs from pruned mechanistic circuits, extending OpenAI's Sparse Circuits

   Python 73 4

5. verifiable-transformers verifiable-transformers Public

   SMT-encodable GPT-2 variant with formal guarantees

   Python 14 1

6. priorproof priorproof Public

   Measure technique novelty for formal (Lean) proofs

   Python