Academy of Mathematics and Systems Science, UCAS
Ph.D. in Applied Mathematics
Research: AI for Mathematics · Advisor: Prof. Lihong Zhi
Greetings! This is Hao Shen
B.Sc. WHU (2020–2024) · Ph.D. UCAS (2024–Present)
I am a Ph.D. student in Applied Mathematics at the Academy of Mathematics and Systems Science, Chinese Academy of Sciences, and the University of Chinese Academy of Sciences. I am fortunate to be advised by Prof. Lihong Zhi.
After receiving my B.Sc. in Statistics from Wuhan University, I began my doctoral studies at AMSS in 2024. I also worked as an algorithm research intern at StepFun, focusing on autoformalization and automated theorem proving.
My research lies at the intersection of formal mathematics, symbolic computation, and artificial intelligence. I develop automated tools, powered by formal methods and large language models, to make mathematical reasoning more scalable, reliable, and verifiable.
Please feel free to contact me via: shenhao24@amss.ac.cn
What’s new
- Google DeepMind updated IMO Bench to address the issues we identified in two geometry problems, PB-Basic-028 and PB-Advanced-010, and thanked the MechGeo Research Team for reporting the formalization mistakes.NEW
- New work: Our paper MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4 is now on arXiv.
- Our Wu–Ritt characteristic-set formalization was presented at the Lean Workshop, affiliated with ITP 2026 at FLoC.
- Our papers on formalizing the Wu–Ritt characteristic-set method and automated tactics for polynomial reasoning were accepted at ICMS 2026 and presented in its Proof Assistants, CAS, and AI session.
- Our extended abstract Certified CAS-assisted Polynomial Reasoning in Lean 4 appeared in the proceedings of SCML 2026 and was presented at the conference.
Earlier news
- Our work Formalizing Wu-Ritt Method in Lean 4 became available as a preprint.
- We released Automated Tactics for Polynomial Reasoning in Lean 4.
- Our formalization of Gröbner Basis Theory in Lean became available on arXiv.
Education
Wuhan University
B.Sc. in Statistics
Featured Publications
My name is shown in bold. For the complete and current citation record, please see my Google Scholar profile.
A Dimension-Independent Commutator Bound
Preprint, 2026.
A dimension-independent operator-norm bound for commutator representations of trace-zero matrices, with the main results and essential inputs formalized in Lean 4.
MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
Preprint, 2026.
A Mathlib-native agentic framework for faithful autoformalization, certified proof construction, and counterexample-guided diagnosis in Euclidean geometry.
Formalizing the Wu-Ritt Characteristic Set Method in Lean 4
International Congress on Mathematical Software (ICMS 2026).
Formal foundations for characteristic sets, pseudo-division, triangular decomposition, and certified polynomial-system solving.
Automated Tactics for Polynomial Reasoning in Lean 4
International Congress on Mathematical Software (ICMS 2026).
Certificate-based tactics connecting external computer algebra systems with formal verification in Lean 4.
Formalizing Gröbner Basis Theory in Lean
Preprint, 2026.
A Mathlib formalization covering polynomial division, Buchberger’s criterion, and reduced Gröbner bases over infinitely many variables.
Research Experience
- Apr. 2024–
Feb. 2025Algorithm Research Intern · StepFun
Building and training neural networks; research on autoformalization and automated theorem proving.
- 2022–2023
Computer Vision Research
Self-supervised learning, weakly-supervised learning, and visual representation learning.
GitHub Stats
 |
 |
GitHub statistics are being generated. View my GitHub profile ↗ · Run the stats workflow ↗
Selected Honors
- 2025
National Scholarship
Ministry of Education, China
- 2024
Outstanding Graduate
Wuhan University
- 2023
National Scholarship
Ministry of Education, China