Pinned

1. lean-dojo/LeanDojo lean-dojo/LeanDojo Public

   Tool for data extraction and interacting with Lean programmatically.

   Python 456 66

2. princeton-vl/CoqGym princeton-vl/CoqGym Public

   A Learning Environment for Theorem Proving with the Coq proof assistant

   Coq 369 50

3. lean-dojo/ReProver lean-dojo/ReProver Public

   Retrieval-Augmented Theorem Provers for Lean

   Python 173 33

4. princeton-nlp/NLProofS princeton-nlp/NLProofS Public

   EMNLP 2022: Generating Natural Language Proofs with Verifier-Guided Search https://arxiv.org/abs/2205.12443

   Python 79 14

5. lean-dojo/LeanDojoChatGPT lean-dojo/LeanDojoChatGPT Public

   ChatGPT plugin for theorem proving in Lean

   Python 99 13

6. lean-dojo/LeanCopilot lean-dojo/LeanCopilot Public

   LLMs as Copilots for Theorem Proving in Lean

   C++ 816 71