Lean-QIT는 양자 정보 이론(QIT)을 위한 Lean 4 라이브러리입니다. 양자 상태, 채널, 코드, 성능 기준, 가설 검정 등 다양한 요소를 형식화하여 제공합니다. 슈마허 양자 소스 코딩 정리, Holevo-Schumacher-Westmoreland 고전 용량 정리 등 핵심 정리들을 검증했습니다. Lean-QIT는 재사용 가능한 운영 정의와 분석적 특성화를 분리하여 양자 정보 분야의 형식화된 기반을 제공합니다.