--- title: "Peiyang Song — author profile and papers — Elamur Research" description: "Peiyang Song, California Institute of Technology: 2 papers on Elamur Research (2023–2024), h-index 3 — affiliations, topics, co-authors and…" canonical: "https://research.elamur.ai/free/en/authors/peiyang-song/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/authors/peiyang-song/) [home](https://md.research.elamur.ai/free/en/) / [authors](https://md.research.elamur.ai/free/en/authors/) / Peiyang Song # Peiyang Song Peiyang Song has 2 papers in our library, in 2023–2024, most of them on [Language models & pretraining](https://md.research.elamur.ai/free/en/topics/language-models/), [Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/), [Information retrieval & search](https://md.research.elamur.ai/free/en/topics/information-retrieval/); often with [Anima Anandkumar](https://md.research.elamur.ai/free/en/authors/anima-anandkumar/), [Kaiyu Yang](https://md.research.elamur.ai/free/en/authors/kaiyu-yang/), [Aidan Swope](https://md.research.elamur.ai/free/en/authors/aidan-swope/). 2 papers in our library · 2023–2024 [OpenAlex](https://openalex.org/A5114152107) · [**h-index 3**](https://openalex.org/authors/A5114152107) · [21 works](https://openalex.org/works?filter=author.id:A5114152107) · [80 citations](https://openalex.org/works?filter=author.id:A5114152107&sort=cited_by_count:desc) OpenAlex, 2026-10-14 [📄 2 works in our library](https://md.research.elamur.ai/free/en/authors/peiyang-song/#papers) · [🔗 Cited 224 times in our library](https://md.research.elamur.ai/free/en/authors/peiyang-song/cited-by/) · [1 more in our library without a page yet](#also) · [⭐ Paper Stars ranking: #5799](https://md.research.elamur.ai/free/en/paper-stars/page/58/#star-5799) The profile is the library's match of the name; two people with one name are not always told apart. Elsewhere: [Google Scholar](https://scholar.google.com/citations?view_op=search_authors&mauthors=Peiyang+Song) · [Semantic Scholar](https://www.semanticscholar.org/search?q=Peiyang+Song) · [dblp](https://dblp.org/search?q=Peiyang+Song) · [ACL Anthology](https://aclanthology.org/search/?q=Peiyang+Song) ## Affiliations [🎓**California Institute of Technology** Pasadena · United States 2024–2026 · 10 papers*current*](https://md.research.elamur.ai/free/en/universities/california-institute-of-technology/) · [🎓**Carnegie Mellon University** Pittsburgh · United States 2026 · 4 papers*current*](https://md.research.elamur.ai/free/en/universities/carnegie-mellon-university/) From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 1 more institution on single bylines are not listed. ## Fields, topics and concepts Of its works in our library, with the number of works on each. 📚 Shelves 6 The field of science this work belongs to (OpenAlex fields).[Computer Science · 2 works](https://md.research.elamur.ai/free/en/shelves/computer-science/) · [Artificial Intelligence · 2 works](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · [Computational Theory and Mathematics · 2 works](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · [Arts and Humanities · 1 work](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · [Language and Linguistics · 1 work](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · [Mathematics · 1 work](https://md.research.elamur.ai/free/en/shelves/mathematics/) 🧭 Topics 3 Research subjects and languages the work is about.[Language models & pretraining · 2 works](https://md.research.elamur.ai/free/en/topics/language-models/) · [Reasoning · 2 works](https://md.research.elamur.ai/free/en/topics/reasoning/) · [Information retrieval & search · 1 work](https://md.research.elamur.ai/free/en/topics/information-retrieval/) 💡 Concepts 1 Key ideas and methods explained on our concept pages.[Retrieval-augmented generation · 1 work](https://md.research.elamur.ai/free/en/concepts/retrieval-augmented-generation/) ## Works by year ### 2020s [**2024** 1 paper](https://md.research.elamur.ai/free/en/authors/peiyang-song/year/2024/) · [**2023** 1 paper](https://md.research.elamur.ai/free/en/authors/peiyang-song/year/2023/) ## Papers The most cited first (OpenAlex and our library). 1. **[LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/)** *(2023 · 253 citations)* Research on machine learning for formal theorem proving has been hard to reproduce and build on. Earlier LLM-based provers kept their code and training data private, and some needed thousands of GPU-days of compute. The authors respond with LeanDojo, an open toolkit for the Lean proof assistant. It uses Lean 3 by… 2. **[Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://md.research.elamur.ai/free/en/papers/song-2024-lean-copilot-large-language-models/)** *(2024 · 39 citations)* Existing LLM-based provers for Lean usually run autonomously on a backend server. They often fail on genuinely new theorems or on mathematical domains outside their training data. This paper instead treats LLMs as assistants that work alongside humans inside Lean itself. The authors present Lean Copilot, a framework… ## All works 3 works of theirs in our library, the most cited first; 2 with a page here, the others link their original until we summarise them. 1. **[LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Kaiyu Yang, Aidan M. Swope, Alex Gu, et al.*2023 · 253 citations* 2. [**Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean arXiv:2404.12534**Peiyang Song, Kaiyu Yang, Anima Anandkumar*2024 · 39 citations*](https://md.research.elamur.ai/free/en/papers/song-2024-lean-copilot-large-language-models/) 3. **[Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skills ↗](https://doi.org/10.4230/lipics.esem.2026.62) arXiv (Cornell University) · no summary yet**Jiang, Pengcheng et al.*2025 · 3 citations* ## Co-authors here 6 co-authors with a page, the most papers together first. - [Anima Anandkumar](https://md.research.elamur.ai/free/en/authors/anima-anandkumar/) ×2 - [Kaiyu Yang](https://md.research.elamur.ai/free/en/authors/kaiyu-yang/) ×2 - [Aidan Swope](https://md.research.elamur.ai/free/en/authors/aidan-swope/) - [Alex Gu](https://md.research.elamur.ai/free/en/authors/alex-gu/) - [Rahul Chalamala](https://md.research.elamur.ai/free/en/authors/rahul-chalamala/) - [Ryan Prenger](https://md.research.elamur.ai/free/en/authors/ryan-prenger/) ## Venues Where their works here were published, the most works first, with the editions of those that have a page. - [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/): [NeurIPS 2023](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/2023/) ## Cited by Papers of our library cite their works 224 times (of the 149,439 papers whose bibliographies we read); [97 citing papers with a page here →](https://md.research.elamur.ai/free/en/authors/peiyang-song/cited-by/). Updated 3 November 2026