Lean 4 통계적 학습 이론 라이브러리

FormalSLT는 유한 샘플 통계적 학습 이론(finite-sample statistical learning theory)을 Lean 4 언어로 형식화한 라이브러리다. 경험적 위험 최소화(ERM)부터 VC 스타일의 일반화 경계(generalization bounds)에 이르는 복잡한 수학적 경로를 기계가 검증할 수 있는 형태로 제공한다.

주요 특징은 다음과 같다:

• 45개의 Lean 모듈로 구성된 체계적인 구조.
• sorry나 admit과 같은 미완성 증명 없이 모든 증명이 기계적으로 검증됨.
• Rademacher 대칭화, Massart 경계, Sauer-Shelah 정리, PAC-Bayes 경계, 알고리즘 안정성 등 핵심 이론을 폭넓게 포함.

이 프로젝트는 기존 논문들의 서술적 증명에서 발생할 수 있는 모호함을 제거하고, 통계적 학습 이론의 핵심 경로를 기계적으로 검증 가능한(machine-checked) 상태로 구축하는 것을 목표로 한다.