著者は、有限次元量子情報理論（QIT）のための再利用可能な運用層を提供するように設計された Lean 4 ライブラリである LeanQIT を提示する。このインフラストラクチャは、情報の理論的定式化とは独立して、符号、誤り基準、達成可能レート、および容量を定義する。

  • 量子状態、チャネル、ソースおよびチャネル符号、仮説検定のための合成可能でカーネルチェック付きのインターフェースを提供する。
  • シュマッハの量子ソース符号化定理、ホレボ・シュマッハ・ウェストモアランドの古典容量定理、およびその強い逆を伴うエンタングルメント支援古典容量定理を形式化する。
  • 運用定義と解析的定式化を分離するために、再利用可能な達成可能性、逆、および漸近的成分を公開する。

Lean-QIT は形式的 QIT の機械可読な基盤を提供し、AI 支援による形式化、自動証明探索、およびエージェント型推論のための合成可能な知識基盤として機能する。