Lean 4における統計的学習理論: ゼロからの経験過程

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

February 2, 2026

著者: Yuanhe Zhang, Jason D. Lee, Fanghui Liu

cs.AI

要旨

本論文では、経験過程理論に基づく統計的学習理論（SLT）の最初の包括的なLean 4形式化を提示する。我々のエンドツーエンドの形式的インフラは、最新のLean 4 Mathlibライブラリで不足していた内容を実装しており、ガウシアン・リプシッツ集中性の完全な構築、部分ガウス過程に対するダドリーのエントロピー積分定理の初の形式化、およびシャープなレートを持つ最小二乗（スパース）回帰への応用を含む。本プロジェクトは、人間が証明戦略を設計しAIエージェントが戦術的証明構築を実行するという、人間とAIの協調ワークフローを用いて実施され、人間によって検証されたSLTのためのLean 4ツールボックスが作成された。実装を超えて、この形式化プロセスは標準的なSLT教科書における暗黙の仮定と欠落した詳細を明らかにし解決し、理論に対する行単位の詳細な理解を強制する。本成果は再利用可能な形式的基盤を確立し、機械学習理論における将来の発展への道を開くものである。コードはhttps://github.com/YuanheZ/lean-stat-learning-theory で公開されている。

English

We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration, the first formalization of 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 to the human-verified Lean 4 toolbox for SLT. Beyond implementation, the formalization process exposes and resolves implicit assumptions and missing details in standard SLT textbooks, enforcing a granular, line-by-line understanding of the theory. This work establishes a reusable formal foundation and opens the door for future developments in machine learning theory. The code is available at https://github.com/YuanheZ/lean-stat-learning-theory