{"id":"arxiv/2602.02285","url":"https://arxiv.org/abs/2602.02285","tags":["cs.LG","cs.CL","math.ST"],"score":0,"title":"AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory","domain":"cs.LG","source":"arxiv","authors":["Yuanhe Zhang","Jason D. Lee","Fanghui Liu"],"reviews":0,"subject":"cs.LG","summary":"We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our en-to-end formal infrastructure implement the missing contents in latest Lean library, including a complete development of Gaussian Lipschitz concentration, Dudley's entropy integral theorem for sub-Gaussian processes, and an application to least-squares (sparse) regression with a sharp rate. The project was carried out using a human-AI collaborative workflow, in which humans design proof strategies and AI agents execute tactical proof construction, leading…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-02","reactions":{}}