LeanDojo

All

5 repositories

LeanCopilot
Public
LLMs as Copilots for Theorem Proving in Lean
machine-learning theorem-proving lean formal-mathematics lean4 llm-inference
C++
•
MIT License
•94•1k•13•0•Updated Jan 4, 2025Jan 4, 2025
LeanDojoWebsite
Public
Code for LeanDojo's website
machine-learning theorem-proving lean lean4
JavaScript
•
MIT License
•2•8•0•0•Updated Jan 3, 2025Jan 3, 2025
LeanDojo
Public
Tool for data extraction and interacting with Lean programmatically.
machine-learning theorem-proving lean lean4
Python
•
MIT License
•94•595•3•3•Updated Jan 2, 2025Jan 2, 2025
ReProver
Public
Retrieval-Augmented Theorem Provers for Lean
machine-learning theorem-proving lean lean4
Python
•
MIT License
•53•239•1•0•Updated Aug 29, 2024Aug 29, 2024
LeanDojoChatGPT
Public
ChatGPT plugin for theorem proving in Lean
machine-learning theorem-proving lean lean4 large-language-models chatgpt chatgpt-plugin
Python
•
MIT License
•13•113•1•0•Updated Apr 4, 2024Apr 4, 2024