PeopleofSuperintelligence

Lab leader

Kaiyu Yang

Also known as 杨凯峪

Kaiyu Yang is a computer scientist whose work links machine learning with formal mathematics. He earned degrees at Tsinghua, Michigan and Princeton, and coauthored research on pose estimation and proof-assistant tools including CoqGym, ASTactic and LeanDojo. He served as a postdoctoral fellow at Caltech and a research scientist at Meta FAIR before joining MiroMind as Lead Scientist of its Verifiable AI Lab in March 2026. Since 2026, he is Lead Scientist at Apodex, where he leads a team on language models for mathematics and verification.

Now at
Apodex
Works
51
Citations
6,356
h-index
10
Badges
Links
Website, Google Scholar, LinkedIn and GitHub

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

  1. 2016

    Stacked-hourglass pose estimation

    In 2016, he coauthors Stacked Hourglass Networks for Human Pose Estimation, a convolutional network that processes body features across multiple scales to estimate human poses.

  2. 2016–2022

    Degrees across three universities

    He earns a B.Eng. in computer science and a B.S. in mathematics at Tsinghua in 2016, an MS in computer science and engineering at the University of Michigan in 2018, and a PhD in computer science at Princeton under Jia Deng in 2022.

  3. 2019

    CoqGym and ASTactic

    With Jia Deng, he introduces CoqGym in 2019, a dataset and learning environment with 71,000 human-written Coq proofs, and ASTactic, a deep-learning model that generates tactics as programs.

  4. 2022–2024

    A Caltech postdoctoral fellowship

    At Caltech, he serves as a postdoctoral fellow in the Computing Data and Society Program from 2022 to 2024, advised by Yisong Yue and Pietro Perona.

  5. 2023

    LeanDojo and ReProver

    In 2023, he coauthors LeanDojo, an open-source Lean playground with toolkits, data, models and benchmarks for language-model theorem proving. Its ReProver model uses retrieval to select premises from a large math library.

  6. 2024–2025

    Meta FAIR and Goedel-Prover

    From 2024 to 2025, he works as a research scientist at Meta Fundamental AI Research (FAIR). In 2025, he coauthors Goedel-Prover, an open-source language model for automated formal proof generation in mathematics.

  7. March 2026

    Leading MiroMind's Verifiable AI Lab

    In March 2026, he joins MiroMind as Lead Scientist of its Verifiable AI Lab and leads work on verifiable reasoning and generation for code and mathematical proofs.

  8. Since 2026

    Lead scientist at Apodex

    Since 2026, he is Lead Scientist at Apodex, where he leads a research team working on large language models for mathematics and verification.

Career

  1. Since 2026ApodexLead Scientist
  2. From 2026MiroMindLead Scientist
  3. 2024–2025FAIR (Meta)Research Scientist
  4. 2022–2024California Institute of TechnologyPostdoctoral Fellow

Education

  1. 2022Princeton UniversityPhD
  2. 2018University of MichiganMS
  3. 2016Tsinghua UniversityB.Eng. and B.S.

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Most-cited works

  1. Stacked Hourglass Networks for Human Pose Estimation2016 · Lecture notes in computer science · 5,616 citationsWith Jia Deng
  2. Towards fairer datasets2020 · 254 citationsWith Fei-Fei Li, Jia Deng and Olga Russakovsky
  3. Infinite Photorealistic Worlds Using Procedural Generation2023 · IEEE Computer Society Conference on Computer Vision and Pattern Recognition · 88 citationsWith Jia Deng
  4. A Study of Face Obfuscation in ImageNet2021 · 87 citationsWith Fei-Fei Li, Jia Deng and Olga Russakovsky
  5. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models2023 · neural information processing systems · 74 citations

From OpenAlex, as of 21 October 2026.

Videos

YouTube videos in which Kaiyu Yang speaks or appears, newest first. A model chose them from YouTube search results. List updated 20 October 2026.

  1. Kaiyu Yang - Formal Reasoning Meets LLMs: Toward AI for Mathematics and VerificationBoston Computation Club · 2 August 2025 · 1 h 14 min
  2. Formal Reasoning Meets LLMs: Toward AI for Mathematics and VerificationSimons Institute for the Theory of Computing · 16 April 2025 · 1 h 5 min
  3. Adv. LLM Agents MOOC | UC Berkeley Sp25 | LMs for Autoformalization+Theorem Proving by Kaiyu YangBerkeley RDI · 13 April 2025 · 52 min
  4. LLM Understanding: 18. Kaiyu YANG "Towards an AI Mathematician"Stevan Harnad · 8 June 2024 · 1 h 15 min

All 5 videos of Kaiyu Yang

Video data from YouTube API Services. By watching you agree to the YouTube Terms of Service. How we use YouTube data.

  1. 16% of AI career moves in the 2020s went from a university to a companyIncludes Kaiyu Yang. We estimate that 16% of AI career moves in the 2020s went from a university to a company; 29% of moves starting at a university went to a company, and 76% ended the university role.
  2. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes Princeton University. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other university. We compare doctorate and 5+ year employment links, career timing and current workplaces for 187 major-prize and 1,111 best-paper winners.
  3. 84% of people shaping AI with recorded undergraduate and doctoral schools changed institutions for their doctorateIncludes Princeton University. 84% of people shaping AI with recorded undergraduate and doctoral schools changed institutions for their doctorate. Across 2,116 people with both an undergraduate degree and a doctorate recorded, we trace which undergraduate schools feed which doctoral programs, how often students stay at the same school, and how paths differ by birth-country region.
  4. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes Meta. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Kaiyu Yang yet. Send us a free-licensed photo.

  1. Stacked Hourglass Networks for Human Pose Estimation arxiv.org. Checked 21 October 2026.
  2. Graduate students receive Siebel Scholar awards engineering.princeton.edu. Checked 21 October 2026.
  3. Kaiyu Yang — Background & Publications yangky11.github.io. Checked 21 October 2026.
  4. Learning to Prove Theorems via Interacting with Proof Assistants proceedings.mlr.press. Checked 21 October 2026.
  5. CDSP Fellows ist.caltech.edu. Checked 21 October 2026.
  6. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models arxiv.org. Checked 21 October 2026.
  7. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving arxiv.org. Checked 21 October 2026.
  8. MiroMind Announces Three World-Class Scientific Leaders to Join Its Core AI Research Team prnewswire.com. Checked 21 October 2026.
  9. Kaiyu Yang yangky11.github.io. Checked 21 October 2026.