LeanDojo: Theorem Proving with Retrieval-Augmented Language Models - Yang, Kaiyu; Swope, Aidan; Gu, Alex; Chalamala, Rahul; Song, Peiyang; Yu, Shixing; Godil, Saad; Prenger, Ryan J; Anandkumar, Animashree (Advances in Neural Information Processing Systems, 2023)