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
•95•1k•12•0•Updated Feb 3, 2025Feb 3, 2025
ReProver
Public
Retrieval-Augmented Theorem Provers for Lean
machine-learning theorem-proving lean lean4
Python
•
MIT License
•55•247•1•0•Updated Jan 30, 2025Jan 30, 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
•95•610•2•3•Updated Jan 2, 2025Jan 2, 2025
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•115•1•0•Updated Apr 4, 2024Apr 4, 2024