LeanDojo: Theorem Proving in Lean using Language Models LLMs as Copilots for Theorem Proving Your browser does not support HTML video. We introduce Lean Copilot for LLMs to act as copilots in Lean for proof automation, e.g., suggesting tactics/premises and searching for proofs. Users can use our model or bring their own models that run either locally (w/ or w/o GPUs) or on the cloud. Overview of LeanDojo Top right: LeanDojo extracts proofs in Lean into datasets for training machine learning mode...