CV

Academic curriculum vitae. Download Academic CV (PDF)

Contact Information

Name Hongwei (Alex) Wang
Professional Title MSc Student in Interdisciplinary Data Science and Artificial Intelligence
Email hw4375@nyu.edu
Website https://hw4375-collab.github.io/

Professional Summary

Master’s student with an academic background in pure mathematics, working across type theory, formalized mathematics, and reliable AI reasoning.

Education

  • 2026 - 2028

    Abu Dhabi, United Arab Emirates

    MSc
    New York University Abu Dhabi
    Interdisciplinary Data Science and Artificial Intelligence
    • Expected completion: August 2028.
  • 2026 - 2026

    United Kingdom

    First Class Honours Bachelor's Degree
    University of Liverpool
    Applied Mathematics
  • 2022 - 2026

    China

    Bachelor of Science
    Xi'an Jiaotong-Liverpool University
    Mathematics
    • Undergraduate dual-degree educational background; the accompanying University of Liverpool entry records the second awarded degree.

Research Experience

MIDSAI Research Participant — Data Science & AI (July 2026–Present): New York University Abu Dhabi · Mentor: Pierre Youssef, CIDSAI. Investigating mathematical autoformalization and semantic faithfulness through controlled evaluation of AI-generated formalizations and Lean-assisted verification workflows.
Topological Quantum Computation Formalization (2026–Present): New York University Abu Dhabi · Academic guidance: Urs Schreiber. Exploring Cubical Agda formalizations of homotopy-theoretic constructions relevant to topological quantum computation.
Categorical Algebra and Homotopy Theory — Final Year Project (2025–2026): Xi'an Jiaotong-Liverpool University · Advisor: Alastair Darby. Studied algebraic topology and homotopy theory from a categorical perspective, connecting these topics with dependent type theory and Lean 4 formalization.
Lean 4 Formalization Benchmark for 1-Category Theory (December 2025): Westlake University and Yau Mathematical Sciences Center, Tsinghua University · Rongge Xu. Constructed and manually verified Lean 4 formalizations of classical results in 1-category theory for evaluating formal proof generation.
AI-Assisted Mathematical Reasoning and Education — Research Assistant (October 2024–April 2025): Xi'an Jiaotong-Liverpool University · Advisor: Jinsong Xu. Developed a Ramsey-type self-play experiment and AI-assisted tools for mathematical problem solving and visualization.
Visiting Scholar (September 2025–March 2026): Westlake University / Institute for Theoretical Sciences · Xing Gu's group.

Selected Projects

Monoidal Category Formalization — Lean 4 (2026): Formalizations involving monoidal categories, categorical constructions, and strictification-related structures using dependent types and Mathlib.
Semantic Boundary — LLM Reasoning Verification and Faithfulness (2026): Controlled benchmarks comparing direct LLM reasoning, self-checking, and Lean-assisted verification, with attention to reasoning errors and semantic mistranslation.
FalconVerifier — AI Reasoning Verification (2026): Public verification prototype that separates model-generated interpretation from deterministic formal verification and records machine-checkable assurance artifacts.
Arabic Pregroup Grammar — Lean 4 (2026): Typed Arabic grammatical representations with pregroup-style types and machine-checkable reductions; initial VSO/SVO examples are formalized as sentence-level proof certificates.

Academic Talks and Activities

When Proof No Longer Means Understanding — New York University Abu Dhabi (5 November 2026): Academic talk on formal correctness and mathematical understanding.
∞-type Café Summer School — Lecturer (August 2026): Three-lecture, six-hour online series on infinity categories and formal reasoning.
AI for Mathematics Seminar — Founder and Lecturer (June 2026): Xi'an Jiaotong-Liverpool University. Organized and taught introductory Lean 4, type theory, and formalized-mathematics material.
Undergraduate Category Theory Seminar — Organizer and Lecturer (2025): Xi'an Jiaotong-Liverpool University. Led a reading seminar based on Tom Leinster's Basic Category Theory.
XJTLU Winter Pure Mathematics Seminar — Founder, Organizer, and Lecturer (2024–2025): Xi'an Jiaotong-Liverpool University.
IWoAT Summer School — Participant (August 2026): Stable Homotopy Theory.

Technical and Mathematical Skills

Formal Methods: Lean 4, Mathlib, formal verification, theorem proving, dependent type theory.
Mathematics: Higher Category Theory, Homotopy Theory, Algebraic Topology, Type Theory, Formal Semantics.
AI and Computing: Python, Git, LLM evaluation, benchmark design, autoformalization, AI reasoning verification.
Additional Tools: LaTeX, Cubical Agda.