저자들은 유한 차원 양자 정보 이론(QIT)을 위해 재사용 가능한 운영 레이어를 제공하도록 설계된 Lean 4 라이브러리인 LeanQIT을 제시합니다. 이 인프라스트럭처는 정보이론적 서술과 독립적으로 부호, 오류 기준, 달성 가능률 및 용량을 정의합니다.
- 양자 상태, 채널, 소스 및 채널 부호, 가설 검정을 위한 합성 가능하고 커널 체크된 인터페이스를 제공합니다.
- 슈마허의 양자 소스 부호화 정리, 홀레보-슈마허-웨스트모어랜드 고전 용량 정리, 그리고 강한 역을 포함하는 얽힘 보조 고전 용량 정리를 형식화합니다.
- 운영 정의와 해석적 서술을 분리하기 위해 재사용 가능한 달성 가능성, 역, 및 점근적 구성 요소를 노출합니다.
Lean-QIT은 형식적 QIT을 위한 기계 판독 가능한 기반을 제공하며, AI 지원 형식화, 자동 증명 탐색 및 에이전트 추론을 위한 합성 가능한 지식 기판 역할을 합니다.