Curriculum Vitae

Education

2022/09–2026/06 | Beijing Institute of Technology | Bachelor of Mathematics (expected)

Grades (by the end of 6th semester)

  • GPA: 3.9 / 4.0 (94)
  • GPA Ranking: 1 / 27
  • Obtain 90+ scores in almost all the core courses in mathematics
  • Obtain 80+ scores in all courses
  • Courses Including: Abstract Algebra (95), Combinatorics (97), Elementary Algebraic Geometry (100), General Topology (99), Differential Manifolds (92), Programming in C (100), Commutative Algebra (ongoing)

Undergraduate Thesis (WIP)

  • Advisor: Prof. Xun Xie (谢迅), BIT
  • Studying Area: Springer correspondence, general linear groups, Young tableaux, Lie algebras

Awards

Date Round Award Issued by
2025/12 2024–2025 Outstanding Student
优秀学生		 Bejing Institute of Technology
2024/12 2023–2024 Outstanding Student
优秀学生		 Bejing Institute of Technology
2023/12 2022–2023 Model Student
优秀学生标兵		 Bejing Institute of Technology

Scholarships

Date Round Scholarship Issued by
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
2023/12 2022–2023 National Scholarship
国家奖学金		 Ministry of Education, PRC
2022–2025 1st–5th semester
(for 5 times)		 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
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
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
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

  • Computer Science: General programming language familiarity (Python / C++ / Web, etc.). Everyday user of collaborative developing tools (Git). Hands-on experience with building static websites (Quarto / Jekyll) and developing lightweight command-line tools. Github Project Showcase

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

  • Algorithms: Once a competitive programmer (OI / ICPC). Familiarity with most of the data structures and algorithms. Codeforces 1951

  • Formalizing Mathematics: Contributor of Mathlib 4. Participated in BICMR–RUC algebra and formalization summer school. Work experience in formalization and annotation in Lean 4.

  • Languages:

    • Chinese: Native
    • English:
      • IELTS Academic 7.5 (8.5 / 8.5 / 6.5 / 6)
      • CET-6 581
      • CET-4 650
      • CET-SET4 A