Elamur Research⌕
☰
home / authors / Kaiyu Yang

Kaiyu Yang

Kaiyu Yang has 3 papers in our library, in 2019–2025, most of them on Reasoning, Language models & pretraining, Information retrieval & search; often with Aidan Swope, Alex Gu, Anima Anandkumar.

3 papers in our library · 2019–2025

OpenAlex · h-index 3 · 6 works · 68 citations OpenAlex, 2026-10-14

📄 3 works in our library · 🔗 Cited 423 times in our library · 2 more in our library without a page yet · ⭐ Paper Stars ranking: #4668

The profile is the library's match of the name; two people with one name are not always told apart.

Elsewhere: Google Scholar · Semantic Scholar · dblp · ACL Anthology

 Fields, topics and concepts

Of its works in our library, with the number of works on each.

📚 Shelves 6The field of science this work belongs to (OpenAlex fields).Computer Science · 3 worksArtificial Intelligence · 3 worksComputational Theory and Mathematics · 3 worksArts and Humanities · 1 workLanguage and Linguistics · 1 workMathematics · 1 work

🧭 Topics 3Research subjects and languages the work is about.Reasoning · 3 worksInformation retrieval & search · 1 workLanguage models & pretraining · 1 work

💡 Concepts 1Key ideas and methods explained on our concept pages.Retrieval-augmented generation · 1 work

 Works by year

2020s

20251 paper20231 paper

2010s

20191 paper

 Papers

The most cited first (OpenAlex and our library).

  1. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (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. Learning to Prove Theorems via Interacting with Proof Assistants (2019 · 90 citations)
    Classical automated theorem provers work in first-order logic and build long, low-level resolution proofs.
  3. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving (2025 · 84 citations)
    Training language models to write machine-checkable proofs is hard because very little mathematics exists in formal form.

All works

5 works of theirs in our library, the most cited first; 3 with a page here, the others link their original until we summarise them.

  1. LeanDojo: Theorem Proving with Retrieval-Augmented Language ModelsConference on Neural Information Processing Systems (NeurIPS)Kaiyu Yang, Aidan M. Swope, Alex Gu, et al.2023 · 253 citations
  2. Learning to Prove Theorems via Interacting with Proof AssistantsarXiv:1905.09381Kaiyu Yang, Jia Deng2019 · 90 citations
  3. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem ProvingarXiv:2502.07640Yong Lin, Shange Tang, Bohan Lyu, et al.2025 · 84 citations
  4. Formal Mathematical Reasoning: A New Frontier in AI ↗arXiv:2412.16075 · no summary yetKaiyu Yang et al.2024 · 49 citations
  5. A Survey on Deep Learning for Theorem Proving ↗arXiv:2404.09939 · no summary yetZhaoyu Li et al.2024 · 46 citations

 Co-authors here

12 of 14 co-authors with a page, the most papers together first.

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

 Cited by

Papers of our library cite their works 423 times (of the 149,439 papers whose bibliographies we read); 59 citing papers with a page here →.

Updated

This page in Markdown → https://md.research.elamur.ai/free/en/authors/kaiyu-yang/