Download
LeanCopilot integrates large language models (LLMs) as copilots for theorem proving in the Lean proof assistant. It assists users by suggesting tactics, premises, and searching for proofs, thereby enhancing the efficiency of formal verification processes. LeanCopilot supports both built-in models from LeanDojo and custom models, offering flexibility for various use cases.
Features
- Integration of LLMs with Lean proof assistant
- Suggestions for tactics and premises
- Automated proof search capabilities
- Support for built-in and custom models
Project Samples
Categories
LLM InferenceLicense
MIT LicenseFollow Lean Copilot
Other Useful Business Software
Fully Managed MySQL, PostgreSQL, and SQL Server
Cloud SQL handles your database ops end to end, so you can focus on your app.
Rate This Project
Login To Rate This Project
User Reviews
Be the first to post a review of Lean Copilot!