Kaiyu Yang is a research scientist in Meta Fundamental AI Research (FAIR) team. His research aims to build AI that can understand and reason about mathematics. To that end, he has focused on using machine learning, especially large language models, to prove theorems in formal environments such as Coq and Lean. Before joining FAIR, he was a postdoctoral scholar at Caltech, working with Pietro Perona, Yisong Yue, and Swarat Chaudhuri. He received a Ph.D. in computer science from Princeton University (advised by Jia Deng) and bachelor's degrees in computer science and mathematics from Tsinghua University.