Kaiyu Yang is a Computing, Data, and Society Postdoctoral Fellow at Caltech. 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. He has received the Siebel Scholar award. Before joining Caltech, he received a Ph.D. in computer science from Princeton University and bachelor's degrees in computer science and mathematics from Tsinghua University.