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. 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 \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.
Reach my homepage for more details. My Github account is @sun123zxy. You may see an overview of my personal projects at Project Showcase.