Формализация теории статистического обучения в Lean 4

Разработчик создал проект на Lean 4 для строгой формализации ключевых концепций теории статистического обучения, включая VC-размерность, границы Радемахера и PAC-Bayes. Цель — построение читаемой цепочки теорем с явными допущениями и полными доказательствами без пропусков. Проект фокусируется на конечных выборках и алгоритмической устойчивости, предлагая альтернативу абстрактным вероятностным подходам.