
A Lean Formalization of the KLS Conjecture with Universal Poincaré Constant at Most 500
KLS history, recent breakthroughs, and a Lean formalization completed in about 24 hours, with a universal Poincaré constant at most 500.
IRSA Faragher Distinguished Postdoctoral Fellow
School of Statistics, University of Minnesota–Twin Cities
I am a postdoctoral fellow in the School of Statistics at the University of Minnesota–Twin Cities (2025–2027). I received my Ph.D. in Statistics from the University of Minnesota in 2025, advised by Adam J. Rothman. In fall 2025, I served as Seminar Coordinator for the School of Statistics Seminar Series.
I have taught statistics for four years, including statistical machine learning; see my teaching page. Here are my publications.
My research spans three connected areas:
Statistics for science. My current research focuses on quantum information science, particularly quantum state estimation and the foundations of quantum computational advantage. I also work on astrostatistics, including modeling and inference for the stochastic gravitational-wave background.
Foundations of AI. I study the theoretical foundations of machine learning, including training dynamics and generative modeling with human feedback.
Statistical theory and methods. My research spans high-dimensional statistics, adaptive experimental design, and random matrix theory.
Inspired by independent groups’ early-October breakthroughs on the Kannan–Lovász–Simonovits (KLS) conjecture, I completed a Lean formalization with a universal Poincaré constant at most 500. Proposed in 1995, KLS is a central problem in high-dimensional probability, convex geometry, geometric functional analysis, and randomized algorithms. Read the blog.
My recent work on uniform hiding and local hafnian anticoncentration represents a significant breakthrough toward establishing quantum advantage in Gaussian boson sampling. Read the explanation.
Invited talk on gravitational-wave inference at Sun Yat-sen University. Slides
Invited talk on adaptive design for quantum state tomography at Tianjin University. Slides
Began the IRSA Faragher Distinguished Postdoctoral Fellowship at the University of Minnesota.

KLS history, recent breakthroughs, and a Lean formalization completed in about 24 hours, with a universal Poincaré constant at most 500.

On Proof, Understanding, and Artificial Intelligence

From photon interference and the permanent to hafnians, including my results on both uniform hiding and local anticoncentration.

From chess and AI coding to scientific discovery: why verification matters, what Lean checks, and how I would organize research with AI and formal proofs.