LeanCopilot embeds LLM capabilities directly into the Lean 4 proof assistant, enabling proof automation through tactic suggestions and autonomous proof search. It provides APIs for tactic generation, premise selection from a knowledge base, and supports both built-in models from the LeanDojo project and custom models running locally or in the cloud. The system targets formal mathematics workflows where LLMs assist human mathematicians by automating routine proof steps.