About

Thomas (Hanwen) Zhu is a MS in Machine Learning student at CMU, working on automating mathematical discovery. He studies how large language models with reasoning ability can be combined with interactive tools that verify mathematical proofs to solve complex math problems. He is advised by Prof. Sean Welleck and Prof. Jeremy Avigad. He co-developed LeanHammer, an automated reasoning tool in Lean combining neural premise selectors and symbolic automation, and miniCTX (ICLR Oral), a benchmark for neural theorem proving in the context of real-world formalization projects. He worked on Seed-Prover, a state-of-the-art neural theorem prover, as a student researcher at ByteDance. Thomas received BA in Mathematics and Computer Science from Oxford, where he graduated top first (rank 1/90) and received the highest CS Gibbs Prize. His future research projects will focus on building the inference-time algorithms and infrastructure to apply LLMs to research-level mathematics.

Education

Carnegie Mellon University

M.S. , Computer Science

Class of 2025

Other Educations

Awards & Publications