Background

Positions

Education

Publications

Also on Google Scholar. * equal contribution, † equal advising.

Open Source

Core developer of:

• LeanDojo — tooling for interacting with Lean from machine learning pipelines
• ReProver — retrieval-augmented theorem prover
• Lean Copilot — LLM inference inside Lean for proof automation
• CoqGym — large-scale learning environment for the Coq proof assistant

Workshops & Tutorials

• The 6th Workshop on Mathematical Reasoning and AI at NeurIPS 2026 (co-organizer)
• The 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025 (co-organizer)
• The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS 2023 (co-organizer)
• Tutorial on Machine Learning for Theorem Proving at NeurIPS 2023 (co-organizer)

Media

• Mathematicians’ Newest Assistants Are Artificially Intelligent — Scientific American, 2024
• Can LLMs Generate Mathematical Proofs that can be Rigorously Checked? — MarkTechPost, 2023
• Exploring the Tradeoff Between Privacy and Algorithm Performance — Princeton Insights, 2022
• Researchers Devise Approach to Reduce Biases in Computer Vision Data Sets — Princeton Engineering News, 2020
• AI Is Biased. Here's How Scientists Are Trying to Fix It — Wired, 2019

Mentoring

• Zhaoyu Li — PhD student at University of Toronto
• Jiacheng Chen — undergrad at South China University of Technology → PhD student at CUHK
• Peiyang Song — undergrad at UCSB and Caltech → PhD student at CMU
• Rahul Chalamala — undergrad at Caltech → researcher at Together AI
• Shixing Yu — master's student at UT Austin → PhD student at Cornell
• Gene Chou — undergrad at Princeton → PhD student at Cornell
• Jacqueline Yau — master's student at Stanford → PhD student at UIUC

Service

• Area Chair — ECCV 2024, ICML 2025 & 2026, NeurIPS 2026
• Reviewer — ICML, NeurIPS, ICLR, JMLR, TPAMI, CVPR, ICCV, ECCV; NSF panel; ERC Advanced Grant; National Academies proceedings on “AI to Assist Mathematical Reasoning”