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 systems such as Coq and Lean. Before joining FAIR, he was a postdoctoral scholar at Caltech. He received a Ph.D. in computer science from Princeton University and bachelor's degrees in computer science and mathematics from Tsinghua University.