양자 정보 이론(Quantum Information Theory, QIT)은 양자 통신, 계산 및 오류 수정의 기반이 되는 양자 정보 처리의 능력과 근본적인 한계를 특징지어 합니다. 이 이론의 코딩 정리들을 형식화하려면 유한 블록 프로토콜, 해석적 부등식, 그리고 점근적 극한을 통합된 기계 검증 프레임워크 내에서 연결해야 합니다. 그러나 기존 개발들은 코드, 오류 기준, 달성 가능한 속도 및 용량을 그 정보 이론적 특징화와 독립적으로 정의하는 재사용 가능한 운영 계층이 부족합니다. 본 연구에서는 유한 차원 QIT를 위한 Lean 4 라이브러리인 LeanQIT을 제시합니다. 이는 양자 상태 및 채널, 소스 및 채널 코드, 유한 블록 성능 기준, 가설 검정, 일회성 양(one-shot quantities), 그리고 점근적 속도 구성에 대한 조합 가능한 커널 검증 인터페이스를 제공합니다. 이 인프라를 사용하여 우리는 슈마허의 양자 소스 코딩 정리(Schumacher's quantum source-coding theorem), 홀레보-슈마허-웨스트모어랜드 고전 용량 정리(Holevo--Schumacher--Westmoreland classical-capacity theorem), 그리고 그 강한 역정리를 포함하는 얽힘 보조 고전 용량 정리(entanglement-assisted classical-capacity theorem)를 형식화합니다. 운영적 정의와 해석적 특징화를 분리하고 재사용 가능한 달성 가능성, 역(converse), 및 점근적 구성 요소를 노출함으로써, Lean-QIT은 형식 QIT을 위한 기계 판독 가능한 기반과 양자 정보 및 계산 분야에서 등장하는 AI 지원 형식화, 자동 증명 탐색, 그리고 에이전트 추론을 위한 조합적 지식 기질(compositional knowledge substrate)을 제공합니다.