nLab Hongwei Wang
Contents
Position
I am a graduate student in the MSc in Interdisciplinary Data Science and AI (MIDSAI) program at New York University Abu Dhabi.
My academic background is in pure mathematics, with research interests in homotopy type theory, higher category theory, and mathematical formalization.
Contact
Research
My research lies at the intersection of mathematical logic, dependent type theory, and higher-dimensional mathematics, with a particular interest in the relationship between mathematical meaning and formal proof.
I am interested in how mathematical structures and arguments can be translated between different mathematical languages while preserving their underlying meaning. In particular, I study the semantic faithfulness of AI-assisted mathematical formalization: how a machine-checkable proof can be explicitly related to the mathematical statement and reasoning from which it originates.
My current work involves homotopy type theory, higher category theory, and formalization in Cubical Agda and Lean. I am also working under the research guidance of Urs Schreiber on the formalization of homotopy-theoretic constructions in Cubical Agda.
More broadly, I am interested in the role of higher-dimensional structures in the foundations of mathematical reasoning, and in how formal methods may reshape the relationship between mathematical proof and mathematical understanding.
Projects
Homotopy Theory in Cubical Agda
Under the guidance of Urs Schreiber, I am working on the formalization of homotopy-theoretic constructions in Cubical Agda, with the aim of developing mathematical materials that connect readable mathematical exposition with machine-checked formal proofs.
An initial example concerns monodromy, formulated through transport in dependent type families. The work includes source-grounded formalization, explicit mathematical dependencies, and correspondences between mathematical statements and Agda declarations.
The longer-term goal is to develop an extensible collection of formalized homotopy-theoretic results that can be reviewed, reproduced, and further developed by other mathematicians.
Semantic Faithfulness and Shadow Mathematics
I am exploring a framework for connecting mathematical exposition with machine-checked formal proofs, particularly in the context of AI-assisted mathematical formalization.
The central idea is to associate formalized statements and proofs with explicit source references, mathematical dependencies, and readable mathematical reconstructions. This provides a basis for examining not only whether a formal proof is accepted by a proof assistant, but also whether it faithfully represents the intended mathematical meaning.
I am particularly interested in the role of human mathematical judgment in this process, and in developing tools that make the interpretation and review of AI-generated formalizations more efficient.
Talks
- When Proof No Longer Means Understanding — Mathematics Club and Program of Mathematics, New York University Abu Dhabi, November 5, 2026.
Last revised on November 9, 2026 at 18:22:22. See the history of this page for a list of all contributions to it.