Profile photo

HAO SHEN

Ph.D. Student  ·  UCAS  ·  AMSS

"Bridging formal mathematics and machine intelligence."

My academic interests lie at the intersection of mathematics, computer science, and artificial intelligence, with a focus on developing automated tools — powered by formal methods and large language models — to advance the frontiers of formalized reasoning and verification.

Education

Ph.D. in Applied Mathematics 2026 – 2029 (expected)
Academy of Mathematics and Systems Science (AMSS), UCAS, Beijing, China
Advisor: Prof. Lihong Zhi  ·  Topic: AI4Math
M.Sc. in Applied Mathematics 2024 – 2026
Academy of Mathematics and Systems Science (AMSS), UCAS, Beijing, China
Advisor: Prof. Lihong Zhi  ·  Topic: AI4Math
B.Sc. in Statistics 2020 – 2024
Wuhan University, Wuhan, China
Major: Statistics

Experience

Self-Supervised Learning & Weakly-Supervised Learning in Computer Vision
2022 – 2023
Research
Self-Supervised Learning Weakly-Supervised Learning Computer Vision
Building and Training Neural Networks & Algorithm Research Intern
Apr 2024 – Feb 2025
StepFun
Focused on autoformalization and automated theorem proving.
Neural Networks Autoformalization Automated Theorem Proving

Research Interests

📐
Formal Theorem Proving
Mechanized verification of mathematical theorems using Lean 4 and Mathlib.
🧮
Symbolic Computation
I'm a member of the AMSS KLMM group, which focuses on symbolic computation.
🤖
LLM for Mathematics
Training and prompting large language models to generate formal proofs.
🧠
Automated Reasoning
Search, synthesis, and planning algorithms for mathematical reasoning agents.

Publications

Formalizing Gröbner Basis Theory in Lean
Preprint
Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi
arXiv preprint arXiv:2602.12772  ·  February 2026
arXiv PDF
Presents a formalization of Gröbner basis theory in Lean 4 using Mathlib, covering polynomial division, Buchberger's criterion, and the existence and uniqueness of reduced Gröbner bases. Notably handles polynomial rings over infinitely many variables.
Automated Tactics for Polynomial Reasoning in Lean 4
Preprint
Hao Shen, Junyu Guo, Junqi Liu, Lihong Zhi
arXiv preprint arXiv:2604.13514  ·  April 2026
arXiv PDF
Proposes a certificate-based approach combining external computer algebra systems (SageMath, SymPy) with formal verification in Lean 4, enabling automated tactics for remainder verification, Gröbner basis checking, ideal equality, and ideal/radical membership.
Formalizing Wu-Ritt Method in Lean 4
Preprint
Yuxuan Xiao, Hao Shen, Junyu Guo, Dingkang Wang, Lihong Zhi
arXiv preprint arXiv:2604.14912  ·  April 2026
arXiv PDF
Formalizes the Wu-Ritt characteristic set method for triangular decomposition of polynomial systems in Lean 4, including pseudo-division, ascending sets, and zero decomposition algorithms — establishing foundations for certified polynomial system solving and geometric theorem proving.

Technical Skills

Programming Languages

Python★★★★★
Lean 4★★★★☆
C++★★★☆☆
R★★★☆☆
MATLAB★★★☆☆

Tools & Others

🐙 Git 📐 Mathlib4 📊 LaTeX 🔥 PyTorch 🤗 Hugging Face 🍁 Maple 🧮 SageMath 🐍 SymPy ✨ Vibe Coding

Honors & Awards

2026 🏆
National Scholarship
Ministry of Education, China
2024 🎓
Outstanding Graduate
Wuhan University
2023 🌟
National Scholarship
Ministry of Education, China

Personal Interests

🏸
Badminton
Casual games & competitive matches
🎵
Music
Listening & appreciating all genres