
A Lean Formalization of the KLS Conjecture with Universal Poincaré Constant at Most 15
KLS history, recent breakthroughs, and a Lean formalization, from the earlier bound 500 to an October 9 release with a universal Poincaré constant at most 15.
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.
Building on independent groups’ early-October KLS breakthroughs, I improved my Lean-verified universal Poincaré bound from 500 to 15, refining the October 8 paper’s bound of 25. Proposed in 1995, KLS is a central problem in high-dimensional probability, convex geometry, geometric functional analysis, and randomized algorithms. Read the blog · GitHub · Zenodo.
My preprint (Theorem 2.3 and Corollary 2.5) resolves the anticoncentration conjecture for independent complex Gaussian hafnians, with Theorem 2.3 verified in Lean 4.
Galin L. Jones introduced me to Karlin’s 1958 conjectured converse on admissibility in exponential families; we resolved it with a counterexample verified in Lean 4.
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, from the earlier bound 500 to an October 9 release with a universal Poincaré constant at most 15.

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.