Personal Information
I'm a Year 4 undergraduate student from School of Mathematics and Physics, Xi'an Jiaotong-Liverpool University (XJTLU).
Trained as a pure mathematics student, my primary research lies in Algebraic Topology and Homotopy Theory. Building upon this foundation, I am actively exploring how deep structural mathematics can serve as a bridge toward Formalized Mathematics, Homotopy Type Theory, and AI-assisted mathematical reasoning.
My long-term goal is to help construct a rigorous pathway from pure mathematics to machine-verifiable knowledge systems. In particular, I am interested in leveraging structural insights from algebraic topology and homotopy theory to enhance AIโs capability in understanding, representing, and reasoning about complex mathematical objects.
Currently, I work with the Lean Theorem Prover to formalize mathematical theories and investigate how formal verification frameworks may integrate with modern AI systems to build reliable, interpretable, and structurally-aware mathematical intelligence.
You can find my CV here: Hongwei Wang CV (Updated 11/09/25). The document provides a reverse-chronological academic summary, while this website offers a detailed narrative of my intellectual development and research journey.
On this website, you can explore my research projects, academic talks, teaching experience, and my evolving exploration from pure mathematics toward formal and AI-driven mathematical systems. If my work aligns with your interests in mathematics, formal verification, or AI research, please feel free to contact me:
Education
B.Sc. in Mathematics and Applied Mathematics (09/2022 - Expected 06/2026)
School of Mathematics and Physics, Xi'an Jiaotong-Liverpool University (XJTLU), Suzhou, China
School of Mathematics and Physics, Xi'an Jiaotong-Liverpool University (XJTLU), Suzhou, China
โ Click to visit XJTLU School of Mathematics and Physics
Visiting Scholar in Westlake University (09/2025 - Expected 03/2026)
Prof. Gu Xing's Group, Institute for Theoretical Sciences, Westlake University, Hangzhou, China
Prof. Gu Xing's Group, Institute for Theoretical Sciences, Westlake University, Hangzhou, China
โ Click to visit Westlake University Institute for Theoretical Sciences
Publications
(See detailed information in the Publications / Writings section)
| Title | Date | Link |
|---|---|---|
| LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories) | Dec 2025 | [GitHub] |
Lean 4 Theorem Prover Codes
| Title | Date | Link |
|---|---|---|
| Formal Algebraic Structures as Machine-Verifiable Mathematical Systems | Jan 2026 | |
| Formalizing Category-Theoretic Structures in Lean 4 | Jan 2026 |
Expository Writings
(See detailed information in the Publications / Writings section)
| Title | Date | Link |
|---|---|---|
| A Unifying Framework of Galois Connections: From Adjoint Functors to Galois Theory and Topological Covering Spaces | Dec 2025 | [PDF] |
| Categorical Algebra and Homotopy Theory (The Homotopic Interpretation of Mathematical Proofs: a Categorical and Type-Theoretic Study of Structural Equivalence) | In Progress | [PDF] |
| An Upper Bound for the Hausdorff Dimension of Fractals under Symmetry Group Action | May 2025 | [PDF] |
| AI-Driven Python Code Generation for Solving Specific Mathematics Problems | Apr 2025 | [PDF] |
| The Futurama Theorem: Group Theory and Permutations in a Body-Swapping Problem | Mar 2025 | [PDF] |
| Introduction to Commutative Algebra: Rings and Ideals | Aug 2024 | [PDF] |
| Poster of Visualizing The Distribution of Prime Numbers | Aug 2024 | [PDF] |
| Arithmetical Functions and Elementary Theorems on the Distribution of Primes | July 2024 | [PDF] |
Academic Experience
Lean 4 Formalization Benchmark for 1-Category Theory
Westlake University & Yau Mathematical Sciences Center, Tsinghua University (12/2025) | Organizer: Prof. Rongge Xu
- Curated a comprehensive collection of classical theorems in 1-Category Theory, establishing a high-quality Lean 4 dataset to evaluate the reasoning capabilities of LLMs in abstract algebra.
- Benchmarked state-of-the-art models including GPT-5.1, Gemini 3.0, and DeepSeek by analyzing their zero-shot and few-shot generation of formal proofs and structural definitions.
- Performed rigorous manual audits and refactoring of AI-generated Lean 4 code to ensure logical soundness and strict alignment with Mathlib 4 library standards.
- Developed a standardized pipeline for formalizing category-theoretic concepts, addressing complex proof bottlenecks related to dependent type theory and categorical constructions.
Categorical Algebra & Homotopy Theory
Xi'an Jiaotong-Liverpool University (09/2025 - Expected 06/2026) | Advisor: Prof. Alastair Darby
- Conducted systematic study of algebraic topology and homotopy theory, developing understanding of fundamental groups, groupoids, covering spaces, and simplicial homology
- Explored connections between category theory and algebraic topology, examining equivalence between van Kampen theorem and groupoid formulations
- Investigated categorical approaches to Galois theory of covering spaces, analyzing connections between topological and algebraic structures
- Studied dependent type theory and used Lean theorem prover to formalize fundamental theorems, completing verification of ฯโ(Sยน) โ โค
Visiting Scholar in Algebraic Topology
Westlake University (09/2025 - Expected 03/2026) | Advisor: Prof. Xing Gu
- Attended graduate-level algebraic topology seminars weekly, deepening understanding of advanced topics
- Studied basic homotopy theory under supervision, conducting undergraduate thesis work
- Engaged in self-directed study of modern algebraic topology using Haynes Miller's lectures
- Examined simplicial homology theory and homotopy theory, focusing on categorical interpretations
Global Mathematics Students' Summer School
Westlake University (06/2025 - 07/2025) | Organizer: Prof. Huayi Chen
- Participated in intensive summer program with daily mathematics discussion sessions
- Studied fundamental structures across multiple fields: information geometry, algebraic geometry, algebraic number theory, elliptic PDE regularity theory, and modular forms
- Organized core theorems and proof techniques for each topic, creating comprehensive study notes
- Developed cross-disciplinary mathematical framework through systematic summarization
Undergraduate Category Theory Seminar
Xi'an Jiaotong-Liverpool University (02/2025 - 05/2025) | Organizer: Prof. Adam-Chrisiaan von
- Mastered category theory fundamentals: categories, functors, natural transformations, limits, representable functors, and Yoneda lemma
- Delivered special lecture on representable functors and Yoneda lemma as student lecturer
- Explained abstract categorical constructions using concrete examples from algebra and topology
- Illustrated concepts through set representations, group actions, and category of presheaves
XJTLU Winter Pure Math Seminar [poster]
Xi'an Jiaotong-Liverpool University (12/2024 - 01/2025) | Organizer: Stud. Hongwei Wang
- Independently sourced guest lecturers, orchestrated the seminar schedule and topics, and designed promotional posters, subsequently securing official endorsement from the School.
- Delivered an in-depth lecture on Galois theory, guiding the audience from its historical origins in solving polynomial equations to its profound conclusion: the unsolvability of the quintic by radicals. The talk meticulously detailed the construction of the Galois group for a polynomial and explained the fundamental Galois correspondence between subfields of a field extension and subgroups of its Galois group.
- Seminar included functional analysis, measure theory, and topology, etc. The program also featured specialized sessions on spectral graph theory and another advanced topic. All session recordings were uploaded to social media platforms, where they garnered significant positive feedback and extensive viewership.
Analytic Number Theory Study
Xi'an Jiaotong-Liverpool University (06/2024 - 09/2024) | Advisor: Prof. Pietro Sgobba
- Studied Tom M. Apostol's Introduction to Analytic Number Theory, mastering arithmetical functions and Chebyshev estimates
- Learned elementary forms of Prime Number Theorem through guided study
- Wrote review paper "Arithmetical Functions and Elementary Theorems on the Distribution of Primes"
- Programmed Python visualizations generating prime number spirals (Ulam, Klauber, Sacks)
- Investigated properties of prime-rich polynomials through computational analysis
Academic Projects
AI in Mathematics Learning Workshop
Xi'an Jiaotong-Liverpool University (10/2024 - 04/2025) | Advisor: Prof. Jinsong Xu
- Designed and coordinated six-month study applying generative programming to pure mathematics
- Developed interactive learning tools for complex analysis, abstract algebra, and topology
- Created machine-learning analysis of Ramsey's Theorem case on Kโ through computer self-play optimization
- Built visualization tool for conformal mappings with automatic singularity detection
- Programmed scalar field visualization with automatic gradient computation and plotting
- Presented findings in report "AI-Driven Python Code Generation for Solving Specific Mathematics Problems"
Stellar Cluster Analysis Project
Xi'an Jiaotong-Liverpool University (10/2022 - 06/2023) | Advisor: Prof. Xiaoying Pang
- Processed Gaia DR3 star catalog data using Python for cleaning and dimensionality reduction
- Applied Gaussian Mixture Model (GMM) to identify member stars of Beehive Cluster
- Identified 387 high-confidence member stars (confidence > 90%) through statistical analysis
- Produced color-magnitude diagram (CMD) for stellar population analysis
- Implemented Self-Organizing Map (SOM) for unsupervised clustering of stellar data
</div>