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
Orchestrate Your AI Agents with Zenflow
Zenflow orchestrates AI agents like a real engineering system. With parallel execution, spec-driven workflows, and deep multi-repo understanding, agents plan, implement, test, and verify end-to-end. Upgrade to AI workflows that work the way your team does.
Rate This Project
Login To Rate This Project
User Reviews
Be the first to post a review of Lean Copilot!
