LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. - Kaiyu Yang; Aidan M. Swope; Alex Gu; Rahul Chalamala; Peiyang Song 002; Shixing Yu; Saad Godil; Ryan J. Prenger; Animashree Anandkumar (NeurIPS, 2023)

Energy Efficient Convolutions with Temporal Arithmetic. - Rhys Gretsch; Peiyang Song 002; Advait Madhavan; Jeremy Lau; Timothy Sherwood (ASPLOS (2), 2024)

In-Context Learning May Not Elicit Trustworthy Reasoning: A-Not-B Errors in Pretrained Language Models. - Pengrui Han; Peiyang Song 002; Haofei Yu; Jiaxuan You (EMNLP (Findings), 2024)

Creative and Context-Aware Translation of East Asian Idioms with GPT-4. - Kenan Tang; Peiyang Song 002; Yao Qin; Xifeng Yan (EMNLP (Findings), 2024)

Towards Large Language Models as Copilots for Theorem Proving in Lean. - Peiyang Song 002; Kaiyu Yang; Anima Anandkumar (CoRR, 2024)

LeanAgent: Lifelong Learning for Formal Theorem Proving. - Adarsh Kumarappan; Mo Tiwari; Peiyang Song 002; Robert Joseph George; Chaowei Xiao; Anima Anandkumar (ICLR, 2025)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean. - Peiyang Song 002; Kaiyu Yang; Anima Anandkumar (NeuS, 2025)

LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction. - Suozhi Huang; Peiyang Song 002; Robert Joseph George; Anima Anandkumar (CoRR, 2025)