Kaiyu Yang leads a research team at Apodex working on large language models for mathematics and verification. His research covers the training stack for mathematics, as well as verifiers for AI outputs such as proofs, code, and training data. He has worked on machine learning for formal mathematics and built open-source tools including LeanDojo. Previously, he was a research scientist at Meta FAIR and a postdoctoral fellow at Caltech. He received a Ph.D. in computer science from Princeton University and bachelor's degrees from Tsinghua University.