Lean Copilot

An interactive Lean assistant offering model-generated tactics, premise selection and proof search.

• Developer / Organization: LeanDojo team and contributors
• Category: Open-source skills & interfaces
• Purpose: Assist interactive Lean proof writing with language models.
• Key features: LLM-assisted tactic suggestions, premise selection and proof search inside Lean.
• Availability: Open-source software; MIT
• License: MIT (source (opens in a new tab))
• Website / Source code: https://github.com/lean-dojo/LeanCopilot (opens in a new tab)
• Version: GitHub release v4.35.0
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01