Formalizing statistical learning theory in Lean 4 [R]

Lean 4에서 통계적 학습 이론을 형식화하는 프로젝트 소개

Lean 4를 사용하여 통계적 학습 이론의 여러 요소를 형식화하는 프로젝트에 대한 소개입니다. 프로젝트는 읽기 쉽고 교육적인 구조의 '정리 사다리'를 구축하는 것을 목표로 하고 있으며, 다양한 이론적 결과물을 포함하고 있습니다. 피드백을 받아들여 정리 및 증명의 구조 개선이 필요하다고 합니다.

Introduction to a project formalizing statistical learning theory in Lean 4.

This article introduces a project focused on formalizing aspects of statistical learning theory using Lean 4. The goal is to create a readable and pedagogically structured 'theorem ladder' for ML theory, encompassing various theoretical results. The author seeks feedback on theorem organization, proof structure, naming decisions, and future formalization targets.