I'm Xingyu Zhong (钟星宇), a Msc student majoring in Mathematics at the National University of Singapore, starting in 2026. I was an undergraduate majoring in Mathematics at Beijing Institute of Technology.
My mathematical interests arose from competitive programming, in which I had been a participant since primary school. Algebra, combinatorics and formalization of mathematics fascinate me the most. Two months before AI struck and changed the landscape of mathematics forever, I was finalizing my undergraduate thesis on the dominance order of the nilpotent orbits in classical Lie algebras, during which I had the chance to witness the rise of AI in my own research: formalizing the most tedious part of my paper took only two days. While AI4Math and formalization methods have become prominent since the summer of 2026, expertise in curated formalization of specialized mathematics is still in short supply. Times change, but I try to convince myself that formalization does not end with green ticks; reliability, integrity and canonicity remain the things that we humans pursue and may contribute to.
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.