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
(expected) 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
(expected) 2025, 5th Zhenyong Fei Scholarship
费振勇奖学金		 School of Mathematics and Statistics, BIT
北京理工大学数学与统计学院
(expected) 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– 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

  • 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

  • Formalization of 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