Welcome

I’m Xingyu Zhong (钟星宇), an undergraduate student major in Mathematics at Beijing Institute of Technology (enrolled in 2022).

My mathematical interest rise from competitive programming, of which I had been a participant since my primary school. Algebra, combinatorics and formalization of mathematics fascinate me the most. As a recreational activity, I like experimenting with academic publishing systems, being an everyday user of LaTeX, Markdown, Pandoc and Quarto.

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