A Central Limit Theorem for High-Temperature SYK Model: A case study on mathematical research using AI and Lean
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≥4, and let ZN(β) 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 Nq/2 −1(log ZN(β)−𝔼[log ZN(β)]) Longrightarrow 𝒩(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.
Related
- Central Limit Theorem for continuous N-particle systems in fixed- and high-temperature: single level
- A Functional Central Limit Theorem For A Rank-Killed Particle System With Persistent Copies
- A central limit theorem for the degree of a random product of Cremona transformations
- A Central Limit Theorem for Coprime Pair Counts in Randomly Translated Disks
- Quenched functional central limit theorem for the random conductance model under minimal moments
BibTeX
@misc{kamijima2026central,
title = {{A Central Limit Theorem for High-Temperature SYK Model: A case study on mathematical research using AI and Lean}},
author = {Yoshinori Kamijima and Shuta Nakajima and Ryoichiro Noda and Kôhei Sasaya},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.18440},
eprint = {2610.18440},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.18440},
}
RIS
TY - UNPB
TI - A Central Limit Theorem for High-Temperature SYK Model: A case study on mathematical research using AI and Lean
AU - Yoshinori Kamijima
AU - Shuta Nakajima
AU - Ryoichiro Noda
AU - Kôhei Sasaya
PY - 2026
DA - 2026/10/27
PB - arXiv
DO - 10.48550/arxiv.2610.18440
UR - https://arxiv.org/abs/2610.18440
AB - 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≥4, 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(β)−𝔼[log Z_N(β)]) Longrightarrow 𝒩(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.
ER -