A Central Limit Theorem for High-Temperature SYK Model
Yoshinori Kamijima, Shuta Nakajima, Ryoichiro Noda, Kôhei Sasaya
math.PR
Oct 13, 2026 · v1
math-ph math.HO
TL;DR
Main CLT proofs for the SYK free energy were formalized in Lean 4 using AI-generated code reviewed by humans, conditional on one annealed free-energy proposition.
Abstract
The Sachdev–Ye–Kitaev (SYK) model is a quantum many-body model of Majorana fermions with all-to-all random interactions. It has attracted wide interest in condensed matter and high-energy physics as a solvable model of non-Fermi liquids and holography. Fix an even integer $q\geq4$, and let $Z_N(β)$ be the partition function of the Gaussian $q$-body SYK model. We prove that for all sufficiently small inverse temperatures $β> 0$, there exists $ρ=ρ(β)>0$ such that \[ N^{q/2 -1}(\log Z_N(β)-\mathbb{E}[\log Z_N(β)]) \Longrightarrow \mathcal{N}(0,ρ^2). \] In addition to the mathematical results, we discuss how the proofs were developed and refined through interaction between human researchers and AI, and we describe the subsequent formalization of the main arguments in Lean 4. This work thus serves as a case study of a research workflow that integrates human insight, AI-assisted exploration, iterative proof refinement, and formal verification.
Problem
The goal is to establish a central limit theorem for the free energy of the Gaussian q-body Sachdev–Ye–Kitaev model at small inverse temperature. The work also serves as a case study of a research workflow combining human insight, AI assistance, and formal verification.
Approach
The partition function is expanded in Hermite polynomial chaos. The second chaos gives the Gaussian fluctuation, and higher chaoses are controlled by a combinatorial Rademacher argument developed with ChatGPT. Known annealed free-energy limits identify the variance. The refined proofs were formalized in Lean 4, with AI generating the code and the authors reviewing it.
Results
For small β, N^{q/2-1}(log Z_N − E log Z_N) converges to N(0, (q!/2)β²(ℓ_q'(β))²). The Lean 4 formalization of the main results is conditional on Proposition 4.2 and is available at github.com/TokyoProbabilityGroup/SYK_CLT.
