About Me

I am a Physics Ph.D. candidate at Harvard University advised by Xi Yin. My research focuses on Lean formalization, the development of reusable formal libraries, and constructive and axiomatic approaches to quantum field theory.

My broader interests include physics-informed learning and robotics.

Publications

A. Mei and M. R. Douglas.
"Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization"
arXiv:2610.20573 (2026).
NeurIPS MATH-AI Workshop 2026.
Submitted to ICLR 2027.

M. R. Douglas, S. Hoback, A. Mei, and R. Nissim.
"Formalization of QFT"
arXiv:2603.15770 (2026).
ICML AI4Math Workshop 2026.

A. L. Fitzpatrick and Z. Mei.
"LSZ in Action: Extracting Form Factors from Correlators Nonperturbatively in 2d φ⁴ Theory"
arXiv:2308.11091 (2023).
JHEP 03, 154 (2024).

Projects

FLMF

math-commons · Apache-2.0 · Private repository

An open-source formalization project building a machine-verified counterpart to the NIST Digital Library of Mathematical Functions in Lean 4. My contribution is the fidelity-verification regime: a two-tier gate in which every machine-generated statement is checked numerically against an independent computational library and back-translated for comparison with the source text before it is marked verified.

OSforGFF

Apache-2.0 · Public repository

The open Lean library accompanying the QFT formalization. Its source files credit me as one of four authors.

GibbsMeasure

random-fields · Private repository

A Lean formalization of Gibbs measures and the two-dimensional Ising phase transition. I am a maintainer with administrative rights, authored the project roadmap, and proved results including Peierls' argument, the GKS and FKG inequalities, the Lee–Yang theorem, and critical-temperature bounds.

OSreconstruction

Public repository

A formalization of Osterwalder–Schrader reconstruction in Lean 4.

Other Research

Tactile Data for Retargeting in Imitation Learning

This project integrates tactile sensing into the imitation learning retargeting process by matching contact force and contact shape between human fingertip sensors and a robotic gripper to verify successful object grasping. The approach addresses retargeting failures in imitation learning by ensuring physically consistent contact during manipulation, improving robustness and task transfer.

Anomalous Dimension For Multi-trace Operators in \(\mathcal{N}=4\) SYM

The project aims to compute tree-level anomalous dimensions of multi-trace operators in \(\mathcal{N}=4\) Super Yang–Mills theory using a Hamiltonian perturbation approach. This approach is intended to simplify calculations, clarify multi-trace operator mixing, and provide a more transparent understanding of the large-N spectrum beyond current correlator-based limits.