{"data":{"slug":"lean-dojo-leancopilot","name":"LeanCopilot","tagline":"LLMs as Copilots for Theorem Proving in Lean","github_url":"https://github.com/lean-dojo/LeanCopilot","owner":"lean-dojo","repo":"LeanCopilot","owner_avatar_url":"https://avatars.githubusercontent.com/u/136513911?v=4","primary_language":"C++","stars":1314,"forks":127,"topics":["formal-mathematics","lean","lean4","llm","llm-inference","machine-learning","theorem-proving"],"archived":false,"github_pushed_at":"2026-08-22T02:14:29+00:00","maintenance_label":"Very active","stars_delta_30d":11,"url":"https://www.graphcanon.com/tools/lean-dojo-leancopilot","markdown_url":"https://www.graphcanon.com/tools/lean-dojo-leancopilot.md","api_url":"https://www.graphcanon.com/api/graphcanon/tools/lean-dojo-leancopilot","graph_url":"https://www.graphcanon.com/api/graphcanon/graph?tool=lean-dojo-leancopilot","description":"LLMs as Copilots for Theorem Proving in Lean","homepage_url":"https://leandojo.org/leancopilot.html","license":"MIT","open_issues":0,"watchers":15,"ai_summary":"A system that employs large language models to assist with theorem proving within the Lean formalization environment, supporting both Lean and Lean4.","readme_excerpt":"## Requirements\n\n* Supported platforms: Linux (priority), macOS (priority), Windows and [Windows WSL](https://learn.microsoft.com/en-us/windows/wsl/install).\n* [Git LFS](https://git-lfs.com/).\n* Optional (recommended if you have a [CUDA-enabled GPU](https://developer.nvidia.com/cuda-gpus)): CUDA and [cuDNN](https://developer.nvidia.com/cudnn).\n* Required for building Lean Copilot itself (rather than a downstream package): CMake >= 3.7 and a C++17 compatible compiler. A downstream package normally downloads a prebuilt release instead of needing these, *except* on a platform we don't publish a release for (e.g. Intel macOS), where it automatically falls back to building from source and so needs them too.\n\n---\n\n### Getting Started with Lean Copilot\n\n#### Tactic Suggestion\n\nAfter `import LeanCopilot`, you can use the tactic `suggest_tactics` to generate tactic suggestions. You can click on any of the suggested tactics to use it in the proof.\n\n\"suggest_tactics\"\n\nYou can provide a prefix (e.g., `simp`) to constrain the generated tactics:\n\n\"suggest_tactics_simp\"\n\n#### Proof Search\n\nThe tactic `search_proof` combines LLM-generated tactics with [aesop](https://github.com/leanprover-community/aesop) to search for multi-tactic proofs. When a proof is found, you can click on it to insert it into the editor.\n\n\"search_proof\"\n\n#### Premise Selection\n\nThe `select_premises` tactic retrieves a list of potentially useful premises. Currently, it uses the retriever in [LeanDojo](https://leandojo.org/) to select premises from a fixed snapshot of Lean and [mathlib4](https://github.com/leanprover-community/mathlib4/tree/3ce43c18f614b76e161f911b75a3e1ef641620ff).\n\n\n\n#### Running LLMs\n\nYou can also run the inference of any LLMs in Lean, which can be used to build customized proof automation or other LLM-based applications (not limited to theorem proving). It's possible to run arbitrary models either locally or remotely (see [Bring Your Own Model](#bring-your-own-model)).\n\n\"run_llms\"","github_created_at":"2023-09-09T01:52:22+00:00","created_at":"2026-07-11T11:43:45.042828+00:00","updated_at":"2026-08-25T00:01:07.160936+00:00","categories":[{"slug":"ai-agents","name":"AI Agents","url":"https://www.graphcanon.com/categories/ai-agents","markdown_url":"https://www.graphcanon.com/categories/ai-agents.md","api_url":"https://www.graphcanon.com/api/graphcanon/categories/ai-agents"},{"slug":"llm-frameworks","name":"LLM Frameworks","url":"https://www.graphcanon.com/categories/llm-frameworks","markdown_url":"https://www.graphcanon.com/categories/llm-frameworks.md","api_url":"https://www.graphcanon.com/api/graphcanon/categories/llm-frameworks"}],"tags":[{"slug":"formal-mathematics","name":"formal-mathematics"},{"slug":"lean","name":"lean"},{"slug":"lean4","name":"lean4"},{"slug":"llm","name":"llm"},{"slug":"llm-inference","name":"llm-inference"},{"slug":"machine-learning","name":"machine-learning"},{"slug":"theorem-proving","name":"theorem-proving"}],"trust":{"provenance":{"is_fork":false,"github_id":689172454,"owner_type":"Organization","methodology":"github_public_v1","parent_repo":null,"near_duplicate_slugs":[]},"computed_at":"2026-08-25T00:01:06.279Z","maintenance":{"label":"Very active","score":96,"methodology":"github_public_v1","releases_90d":3,"days_since_push":2,"last_release_at":"2026-08-19T14:57:00Z","stars_delta_30d":11,"open_issues_delta_30d":-5},"security_summary":{"status":"no_lockfile","scanner":null,"low_count":0,"high_count":0,"last_scan_at":"2026-07-11T11:43:46.195Z","medium_count":0,"scan_profile":"none","critical_count":0}},"capability_facts":{"scan":{"source":"repo_scan","observed_at":"2026-08-25T00:01:06.814Z"},"deploy":{"source":"dockerfile:Dockerfile","self_host":true,"observed_at":"2026-08-25T00:01:06.814Z","managed_saas":false},"languages":{"value":["c++"],"source":"github.language","observed_at":"2026-08-25T00:01:06.814Z"},"has_docker":{"value":true,"source":"dockerfile:Dockerfile","observed_at":"2026-08-25T00:01:06.814Z"},"license_spdx":{"value":"MIT","source":"github.license","observed_at":"2026-08-25T00:01:06.814Z"}},"decision_facts":{"hosting":null,"pricing":null,"requirements":null,"constraints":null,"when_to_use":["Need support with formal proof development in Lean or Lean4 specifically","Seeking to enhance automated reasoning capabilities within a Lean project"],"when_not_to_use":["Working exclusively in theorem provers other than Lean or Lean4","Looking for general-purpose AI programming assistant beyond Lean's domain"],"source":"enrich:decision_facts","observed_at":"2026-07-17T06:20:50.390Z"},"constraint_facets":null,"decision_summary":[{"label":"Adopt for","value":"A system that leverages large language models for theorem proving in the Lean environment."}]}}