Dr. Kaiyu Yang is a Research Scientist at Meta Fundamental AI Research (FAIR), where he focuses 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, 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 in computer science and mathematics from Tsinghua University.