The Fundamental Theorem of Statistical Learning in Three Weeks

In three weeks, I developed a complete Lean 4 mechanization of a realizable binary Fundamental Theorem of Statistical Learning with Claude Opus 4.6, designing the premise and proof strategies and correcting definitions while Claude developed the Lean proofs. The characterization connects PAC learnability, finite VC dimension, finite-advice compression, uniform Rademacher vanishing, and polynomial growth, with a sample-complexity witness. A multiplicative-weights construction replaces exact minimax in Moran–Yehudayoff compression; ghost-sample symmetrization supplies the VC-to-PAC direction. The development also formalizes Gold's theorem, the Littlestone characterization, and measurability separations. It contains 21,745 lines across 53 files, 352 theorem or lemma declarations, and zero active sorry or admit terms. To my knowledge, this is the first complete mechanization of the stated characterization, under explicit regularity assumptions including measurability of all Boolean-valued functions on the domain. Claude's sustained proof construction enabled these foundations and an attention-router investigation I would otherwise not have undertaken.