Hello there!

I’m Xingyu Zhong (钟星宇), an undergraduate student major in Mathematics at Beijing Institute of Technology enrolled in 2022. I will be a master student majoring in Mathematics in the National University of Singapore starting from 2026.

My mathematical interest arise from competitive programming, of which I had been a participant since my primary school. Algebra, combinatorics and formalization of mathematics fascinate me the most. My undergraduate thesis surveys the classification and the dominance order of the nilpotent orbits in classical Lie algebras, which guides me to the rich world of geometric representation theory. With collaboration of AI, some of the results are formalized in Lean 4. As the dawn of the AI productivity revolution breaks over the mathematical community, I embrace with excitement the new horizons it reveals for mathematical research.

Having been coding since my childhood, I still enjoy programming and software development, especially if it benefits mathematical research around me. I have a wide range of programming experience, including competitive programming, formalization of mathematics in Lean 4, web development and command-line tools. My Github account is @sun123zxy. You may see an overview of my personal projects at Project Showcase.

As a recreational activity, I like experimenting with academic publishing systems, being an everyday user of LaTeX, Markdown, Pandoc and Quarto. An obsession with Markdown has led me to maintain \(\mathrm{\SunQuarTeX}\), a Quarto template for multi-purpose academic writing in Chinese and English, which has gained a small user base since its release in 2022.

Talks

Date Title Links
2026/06/02 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