Kaiyu Yang is a Research Scientist at Meta Fundamental AI Research (FAIR), working on enhancing AI's capabilities in mathematical reasoning by integrating formal systems such as Lean. His research explores how machine learning and large language models can generate mathematical conjectures, prove theorems, write verifiable code, and perform reasoning that combines natural and formal languages. 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 from Tsinghua University.