TY - RPRT TI - Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean AU - Peiyang Song AU - Kaiyu Yang AU - Anima Anandkumar PY - 2025 UR - https://arxiv.org/abs/2404.12534 ID - 2404.12534 ER -