Hi! I am Thomas (Hanwen) Zhu. I am a research scientist at ByteDance Seed working on Seed-Prover.

I obtained MS in Machine Learning student at CMU, working on applying language models to formal theorem proving. I am honored to have been advised by Prof. Sean Welleck and Prof. Jeremy Avigad. I developed miniCTX, LeanHammer, and LeanArchitect at CMU.

I worked on Seed-Prover (V1), which solved 5/6 problems on IMO 2025 and set new state-of-the-art scores on all Lean benchmarks.

I received BA Mathematics and Computer Science from Oxford, where I graduated top first. I had the privilege to work with Ruining Li and Tomas Jakab at VGG in applying diffusion models to 3D generation of human-object interactions. I also worked at OxAI in developing a benchmark for gender bias in large vision-language models.

I was a 2026 Siebel Scholar and I received the highest 2024 Gibbs Prize in Computer Science at Oxford.

Please contact me at [email protected].

Publications

LeanArchitect: Automating Blueprint Generation for Humans and AI
Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck
Paper GitHub

Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
ByteDance Seed
Paper GitHub

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
ByteDance Seed
Paper News GitHub

Premise Selection for a Lean Hammer
Thomas Zhu*, Joshua Clune*, Jeremy Avigad†, Albert Q. Jiang†, Sean Welleck†
Website Paper GitHub
In preprint

miniCTX: Neural Theorem Proving with (Long-)Contexts
Jiewen Hu, Thomas Zhu, Sean Welleck
Website Paper Dataset
ICLR 2025 Oral (Top 1.8%)

DreamHOI: Subject-Driven Generation of 3D Human-Object Interactions with Diffusion Priors
Thomas Zhu, Ruining Li*, Tomas Jakab*
Website Paper GitHub
ICCV HiGen Workshop 2025 Oral

VisoGender: A dataset for benchmarking gender bias in image-text pronoun resolution
Siobhan Mackenzie Hall, Fernanda Gonçalves Abrantes, Thomas Hanwen Zhu, Grace Sodunke, Aleksandar Shtedritski, Hannah Rose Kirk
Paper GitHub
NeurIPS Datasets and Benchmarks 2023

Blogs

May 4, 2025: DeepSeek-Prover-V2 Learned to Cheat.