Hello there!

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

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. 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/07/21 广义纯正九莲宝灯听牌型的唯一性
A Mahjong Game Formalization		 onsite (zh)
  • Final report of 2026 AI4MATH Summer School at Zhejiang University
  • In this talk I shared my recent AI4Math & Lean 4 formalization exploration on a well-known folklore result in Mahjong players: There is no full-sided wait other than the so-called “Nine Gates” suit.
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: Xun Xie (谢迅, BIT)
2026/05/28 Nilpotent Orbits in Classical Lie Algebras
经典李代数中的幂零轨道		 onsite (zh)
  • Undergraduate thesis defense presentation at BIT
  • Advisor: Xun Xie (谢迅, BIT)
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)
  • 2025 spring Algebraic Geometry final presentation
  • Lecturer: Yangyu Fan (范洋宇, BIT)
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 fall Advanced Algebra II course seminar
  • Lecturer: Peng Cao (曹鹏, BIT)
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 spring Mathematical Analysis II course seminar
  • Joint work with Chong Ning (宁冲)
  • Lecturer: Zhentao Lv (吕珍涛, BIT)
2023/04/23 Wallis Product, Stirling’s Approximation and Guassian Distributions
Wallis 公式、Stirling 公式与正态分布		 onsite (zh) / latest (zh)
  • 2023 spring Mathematical Analysis II course seminar
  • Lecturer: Zhentao Lv (吕珍涛, BIT)
2022/12/13 Topics on the compactness of \(\mathbb R\)
有限覆盖定理与实数理论		 latest (zh)
  • 2022 fall Mathematical Analysis I course seminar
  • Lecturer: Pengshuai Shi (史鹏帅, BIT)

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: Feng Zhang (张峰, 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: 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 Yangyu Fan (范洋宇, BIT).
  • 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
2026/07/15–2026/07/21 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 functional & meta programming in Lean 4.
  • Role: Attendance. Made a formalization project presentation there.
  • Organizer: Binyong Sun (孙斌勇, ZJU), Tao Luo (罗涛, SJTU) (SJTU), Jiajun Ma (马家骏, XMU)
  • Lecturer: Anjie Dong (董安杰, CUHK-Shenzhen), Tianyi Xu (徐天一, PKU), Yutong Wang (王语同, PKU)
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)
  • 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.
  • Role: Attendance in the first and the second stage. Lead a group formalization project with final presentation.
  • Lecturer: Riccardo Brasca (Université Paris Cité), Shanwen Wang (王善文, RUC), Huayi Chen (陈华一, WestLake University)
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:, Jose Hernandez-Lobato (University of Cambridge), Jiajun He, (何佳峻, University of Cambridge)
2024/09/30 ComBIT24–StanleyFest link (zh/en)
  • A conference on combinatorics at BIT in 2024
  • Role: Attendance
  • Organizer: David Guoliang Wang (王国亮, BIT)
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