Haocheng Wang (王浩丞)

PhD @ HKUST(GZ) | Visiting Researcher @ ETH Zürich

I am a PhD student at HKUST(GZ) and a Visiting Researcher at ETH Zürich, focusing on formal mathematical reasoning and autoformalization.

日拱一卒 · Keep bounding the rock

Email GitHub Google Scholar CV
Haocheng Wang

About Me

I am a direct doctoral student at DSA Thrust, HKUST(GZ) supervised by Prof. Zhijiang Guo. Currently, I am a Visiting Researcher at ETH Zürich (D-INFK), working with Prof. Rasmus Kyng and Dr. Sorrachai Yingchareonthawornchai on verifiable autoformalization and formal reasoning in Theoretical Computer Science. Previously, I was a Student Researcher at ByteDance Seed and DeepSeek AI.

I graduated with a Bachelor's degree (Honours) in Mathematics and Applied Mathematics from Xiamen University in 2025. My undergraduate thesis focused on formalizing Auction Theory in Lean 4 with Mathlib4, supervised by Prof. Ma Jiajun.

Research Interests

My research focuses on:

News

Mar. 2026Our 3rd AI4Math Workshop at ICML 2026 has been accepted!
Jan. 2026Started as a Ph.D. student at HKUST(GZ), DSA Thrust, supervised by Prof. Zhijiang Guo.
Aug. 2025Joined ETH Zürich (D-INFK) as a Visiting Researcher, working with Prof. Rasmus Kyng and Dr. Sorrachai Yingchareonthawornchai.
Jan. 2025Joined ByteDance Seed as a Student Researcher.
Jun. 2024Joined DeepSeek AI as a Student Researcher.

Featured Projects

DeepSeek-Prover-V2

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

Z.Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z.F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, Chong Ruan

671B-sized model achieving SOTA on miniF2F (88.9%) and PutnamBench (47/658) via RL with subgoal decomposition.

Paper Model Code
ArXiv Preprint, 2025
DeepSeek-Prover-V1.5

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, Chong Ruan

Hybrid approach combining LLMs and Monte-Carlo tree search. SOTA on miniF2F (63.5%) and ProofNet (25.3%).

Paper OpenReview Code
ICLR 2025
Formal Math

Solving Formal Math Problems by Decomposition and Iterative Reflection

ByteDance Seed Team

Training-free agent framework enabling general-purpose LLMs to solve complex formal proofs in Lean 4.

Paper Code
ArXiv Preprint, 2025

Professional Experience

Scientific Assistant I
ETH Zürich
Aug 2025 - Present · Zürich, Switzerland
  • Focusing on building Multi-gLLM Agent for formal reasoning in Theoretical Computer Science
Student Researcher
ByteDance Co., Ltd.
Jan 2025 - Jul 2025 · Shanghai, China
  • Built Scoring & Self-refinement agent pipeline for Natural Language Proof
  • Proposed sketch-incorporated long Chain-of-Thought formal reasoning method
  • Led data initiatives for DeltaProver
Student Researcher
DeepSeek AI Co., Ltd.
June 2024 - Sep 2024 · Beijing, China
  • Developed ProverBench, a domain-categorized benchmark with 325 problems for evaluating LLM theorem proving
  • Contributed to DeepSeek-Prover-V1.5 and V2 model development

Education

Xiamen University

Sep 2020 - Jun 2025

Bachelor of Science in Mathematics and Applied Mathematics (Honours)

Final Thesis: Formalization of Auction Theory using Lean 4 and Mathlib4
[GitHub]

Academic Service

Program Chair

Area Chair

Conference Reviewer

Teaching Assistant

Engagements

Invited Talks

Workshops

Contact

Feel free to reach out to me:

haocheng.wang [at] inf.ethz.ch

hcwang942 [at] gmail.com

OAT Z28, Andreasstrasse 5, Zürich

Visitor Map