1 Introduction

This is the mathematical blueprint for a Lean 4 formalization of the fundamental theorem of statistical learning. It sits between two other artifacts: the kernel source code at https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel, which contains 354 machine-checked theorems in 21,728 lines with zero sorry, and a companion textbook on formal learning theory from which most of the exposition in Chapters 3 through 6 is imported directly. The blueprint’s role is to annotate informal mathematical statements with hyperlinks into the formal declarations that prove them, so that a reader can click from a theorem in prose to the corresponding theorem or def in the Lean kernel and back.

Every statement carrying a \lean{} annotation in this document resolves to a proved declaration in the kernel. The formalization targets Lean 4 v4.29.0-rc6 against mathlib4 pinned at commit fde0cc5. The per-module API reference is at https://zetetic-dhruv.github.io/formal-learning-theory-kernel/.