@misc{indiciaed3d127fea921, title = {Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean}, author = {Peiyang Song and Kaiyu Yang and Anima Anandkumar}, year = {2025}, url = {https://arxiv.org/abs/2404.12534}, note = {Source identifier: 2404.12534} }