Curriculum Vitae

Education

2022/08–2026/06 | Beijing Institute of Technology | Bachelor of Mathematics

GPA: 3.9 / 4.0 (94) GPA Ranking: 1 / 27

90+ scores in most core mathematics courses; 80+ scores in all courses

Courses Including: Commutative Algebra (99), Elementary Algebraic Geometry (100), Combinatorics (97), Abstract Algebra (95), General Topology (99), Programming in C (100), Lie algebras, Representation Theory, etc.

Thesis Advisor: Prof. Xun Xie (谢迅), BIT

Studying Area: Nilpotent orbits; Springer fibers and its combinatorics; Classical Lie algebras; AI4Math and formalization of Mathematics

Introduction: My undergraduate thesis surveys the classification of nilpotent orbits in the classical Lie algebras over \(\mathbb C\), the closure order on these orbits, and the corresponding dominance order on partitions. To the best of our knowledge, proofs in the literature of the equivalence between the dominance order on partitions and the closure order on nilpotent orbits are scattered and lack a unified presentation. We develop a new diagrammatic method for constructing algebraic curves connecting nilpotent orbits of different Jordan types, which streamlines the cumbersome notation in existing approaches and offers a clearer guide to the constructive arguments. In addition, motivated by the historical difficulty of the case-by-case analysis for cover relations in the dominance order of admissible partitions of classical types, we also formalize these cover relations in Lean 4, providing a practical example of human-AI collaboration for modern mathematical formalization.

Links: thesis (zh) / slide (zh)

Date Round Award / Scholarship Issued by
2026/06 2025–2026 Outstanding Graduate (Provincial)
北京市普通高等学校优秀毕业生		 Beijing Municipal Education Commission
北京市教育委员会
2026/06 2025–2026 Outstanding Graduate of BIT
北京理工大学优秀毕业生		 Bejing Institute of Technology
北京理工大学
2025/12 2025, 5th Zhenyong Fei Scholarship
费振勇奖学金		 School of Mathematics and Statistics, BIT
北京理工大学数学与统计学院
2025/11 2024–2025 Baosteel Scholarship for Outstanding Students
宝钢优秀学生奖		 Baosteel Education Foundation
宝钢教育基金会
2025/03 2024–2025 Samsung Scholarship Samsung Electronics China
2024/12 &
2025/12		 2023–2024 &
2024–2025		 Outstanding Student
优秀学生		 Bejing Institute of Technology
北京理工大学
2023/12 2022–2023 Model Student
优秀学生标兵		 Bejing Institute of Technology
北京理工大学
2023/12 2022–2023 National Scholarship
国家奖学金		 Ministry of Education, PRC
教育部
2022–2025 1st–5th semester
 First Class Scholarship
校一等奖学金		 Bejing Institute of Technology
北京理工大学

Competitions

Competitive Programming

ICPC

International Collegiate Programming Contest

Date Competition Prize
2024/11/03 2024 Asia Nanjing Regional Bronze Medal
2023/11/25 2023 Asia Hefei Regional Silver Medal
2023/10/22 2023 Asia Xi’an Regional Bronze Medal
CCPC

China Collegiate Programming Contest

Date Competition Prize
2024/11/17 2024 Zhengzhou National Silver Medal
2024/05/26 2024 Guangdong National Invitational Gold Medal
2023/11/05 2023 Harbin National Silver Medal
2023/05/28 2023 Hunan National Invitational Silver Medal
  • Countless other university / provincial / national contests (BITPC, Baidu Astar, Lanqiao, etc.) in 2022–2024

Mathematics

Date Competition Prize
2024/04/15 2024 Alibaba Global Mathematics Competition Finalist
2022/10 2022 BIT Campus Mathematics Competition for Junier Grade Group First Prize
CMC

The Chinese Mathematics Competitions

Date Competition Prize
2024/11/09 2024 National Preliminary Beijing (Mathematics Major, Type A) Third Prize
2024 Beijing Provincial (Mathematics Major, Type A) Third Prize
2023/11/11 2023 National Preliminary Beijing (Mathematics Major, Type A) Third Prize
2023 Beijing Provincial (Mathematics Major, Type A) Second Prize

Modeling

Date Competition Prize
2023/08 2023 National Collegiate Contest on Statistical Modeling, Beijing Preliminary, Undergraduate Group Second Prize

Talks

Date Title Links
2026/06/03 AI-Assisted Formal Mathematics with Lean 4
 onsite (en)
  • A meeting talk at BIT on the use of agentic tools in mathematical formalization with Lean 4, and its potential impact on mathematical research. The talk is based on my practical experience in formalizing my undergraduate thesis.
  • Invited by: Prof. Xun Xie (谢迅), BIT
2026/05/28 Nilpotent Orbits in Classical Lie Algebras
经典李代数中的幂零轨道		 onsite (zh)
2025/09/17 Introduction to Formal Mathematics with Lean 4 onsite (en) / latest (en)
2025/09/11 Classification of Quadratic Forms over \(\mathbb Q\) onsite (en)
2025/06/20 Irreducible Representations of the Symmetric Group onsite (en) / latest (zh)
  • Selection presentation for UTokyo–BIT Student Math Workshop
2025/04/16 Classification of Quadratic Forms over \(\mathbb Q\) onsite (en) / latest (en)
2024/04/20 DFT from the Perspective of Algebra Isomorphism
代数同构视角下的离散 Fourier 变换		 onsite (zh) / latest (zh)
2023/10/18 The \(\Delta\) Discriminant of Univariate Polynomials
一元多项式的 Delta 判别式		 onsite (zh) / latest (zh)
2023/08/01 A Convolution-Oriented FFT Tutorial onsite (zh) / latest (zh) /
suppliment (zh)
2023/05/18 Space Filling Curves and Cardinality
空间填充曲线与集合势理论		 onsite (zh) / latest (zh)
2023/04/23 Wallis Product, Stirling’s Approximation and Guassian Distributions
Wallis 公式、Stirling 公式与正态分布		 onsite (zh) / latest (zh)
2022/12/13 Topics on the compactness of \(\mathbb R\)
有限覆盖定理与实数理论		 latest (zh)

Programs

Date Program Links
2022/12–2023/12 On the Uniqueness of the DFT matrix
将循环卷积转化为乘积的矩阵是否只有傅里叶矩阵？
  • Innovation and Entrepreneurship Training Program for College Students (Level: Provincial & Collegiate)
    大学生创新创业训练计划（市、校级）
  • It is shown that the DFT matrix, in some degree, is the only linear transformation that carries circulant convolution into pointwise multiplication.
  • Role: Project Leader
  • Advisor: Prof. Feng Zhang (张峰), School of Information and Electronics, BIT

Volunteering

Date Event Links
2026/04/11 Liangxiang Number Theory Conference 2026
  • A conference on the calculus of L-functions at BIT in 2026.
  • Role: Volunteer. Helping with the onsite organization of the conference.
  • Organizer: Prof. Yangyu Fan (范洋宇), BIT
2025/09–2025/12 Introduction to Formal Mathematics with Lean 4 lecture notes (en) /
online notes (en) /
online repository
  • A hobby course introducing the basics of formalization and the Lean 4 interactive theorem prover to undergraduates at BIT. This course is designed to be a companion to the 2025 Fall Abstract Algebra course at BIT lectured by Prof. Yangyu Fan (范洋宇).
  • Role: Organizer / Lecturer
2024–2025 Multiple student-organized seminar on mathematics
  • Role: Organizer / Speaker. Among the organizers of the after-class seminar of the courses Real Variable Functions, Complex Variable Functions and Abstarct Algebra. Among the speakers of the student-organized seminar on Commutative Algebra.
2023–2024 Multiple competitive programming contests
  • Role: Problem Setter. Participated in the problem setting work of 2023 BITCPC and 2024 ICPC Asia Kunming Regional.
2023/07–2023/08 2023 BITACMCLUB competitive programming summer training news (zh)
  • A 5-week training program for BIT & Yan’an Univ. students interested in competitive programming.
  • Role: Lecturer. Talked about DFT / FFT, its convolutional nature and mathematical background.

Work Experience

Date Event Links
2025/07–2025/12 BICMR–Ubiquant AI4Math Internship (Data Annotation Team)
  • Annotating and Formalizing definitions and theorems in abstract algebra via the Lean 4 interactive theorem prover.

Events

Date Event Links
(expected) 2026 AI4MATH Summer School at Zhejiang University
 register (zh)
  • A summer school held by Institute for Advanced Study in Mathematics (Zhejiang University), Xiamen University and Shanghai Jiao Tong University. It’s advanced program includes lectures on meta programming in Lean 4.
  • Role: Attendance
2026/06 PKU Lean 4 Formalization and Code Review Workshop
北京大学 Lean4 形式化代码评审培训工作坊		 register (zh)
  • A weekend workshop held in Peking University on code review and best practices for formalization in Lean 4. Focus: mathlib infrastructure, formalization taste, code review
  • Role: Attendance
2025/09/08–2025/09/12 UTokyo–BIT Student Math Workshop news (zh)
  • Role: Attendance
2025/07/01–2025/07/20 BICMR–RUC algebra and formalization summer school
代数与形式化数学暑期学校		 register (zh) / news (zh) / group project
  • A two-stage summer school held in Renmin University of China and Beijing International Center for Mathematical Research, providing lectures on the Lean prover and some algebra courses. Group presentations on hands-on formalization projects were required in the second stage.
  • Role: Attendance in the first and the second stages
  • Lecturer:
2025/02/02–2025/02/15 2025 FRP winter programme in mordern advanced deep learning
  • A two-week winter program held in University of Cambridge on modern deep learning theories. Group presentations on hands-on projects were required at the end of the program.
  • Role: Attendance / Special Award Winner (3 out of 15)
  • Lecturer:
2024/09/30 ComBIT24–StanleyFest link (zh/en)
2024/04/20–2024/04/21 USTC–BIT Student Math Workshop news (zh)
  • A communication activity between BIT and University of Science and Technology of China
  • Role: Speaker / Attendance

Skills

  • Formal Languages General programming language familiarity. (Python / Lean 4 / C++ / Web, etc.)

  • Algorithm Once a competitive programmer (OI / ICPC). Codeforces 1951

  • Formalizing Mathematics Contributor of Mathlib 4. Work experience in formalization and annotation in Lean 4.

  • Typesetting Experienced user of Markdown, LaTeX, and publishing systems (Pandoc / Quarto). Experience in developing Quarto Lua filters and extensions.

  • Command Line Tools Hands-on experience with developing lightweight command-line tools (Python)

  • Web Frontend Hands-on experience with HTML / CSS / JS, static websites (Quarto / Jekyll), and web scraping. Vibe coding experience in frontend frameworks (Node.js / React).

  • Web Backend / Linux Hands-on experience with lightweight server / proxy deployment and maintenance. A very little experience with asynchronous programming and backend development (FastAPI).

  • Git Everyday user. Github / Project Showcase

  • Natural Languages Native Chinese speaker. English:

    IELTS Academic 7.5 (8.5 / 8.5 / 6.5 / 6)

    CET-6 581

    CET-4 650

    CET-SET4 A