LeanDojo

All

5 repositories

LeanDojo
Public
Tool for data extraction and interacting with Lean programmatically.
machine-learning theorem-proving lean lean4
Python
•
MIT License
•96•617•3•3•Updated Feb 12, 2025Feb 12, 2025
LeanCopilot
Public
LLMs as Copilots for Theorem Proving in Lean
machine-learning theorem-proving lean formal-mathematics lean4 llm-inference
C++
•
MIT License
•98•1k•13•0•Updated Feb 3, 2025Feb 3, 2025
ReProver
Public
Retrieval-Augmented Theorem Provers for Lean
machine-learning theorem-proving lean lean4
Python
•
MIT License
•56•256•2•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
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•114•1•0•Updated Apr 4, 2024Apr 4, 2024