Авторы представляют LeanQIT, библиотеку Lean 4, предназначенную для обеспечения многоразового операционного слоя для квантовой информационной теории (QIT) конечной размерности. Эта инфраструктура определяет коды, критерии ошибок, достижимые скорости и пропускные способности независимо от их информационно-теоретических характеристик.
- Предоставляет композируемые интерфейсы с проверкой ядра для квантовых состояний, каналов, источников и канальных кодов, а также проверки гипотез.
- Формализует теорему Шумахера о квантовом кодировании источника, теорему Холево--Шумахера--Вестморленда о классической пропускной способности и теорему о классической пропускной способности с помощью запутанности с ее сильным обратным утверждением.
- Предоставляет многоразовые компоненты достижимости, обратного утверждения и асимптотики для разделения операционных определений от аналитических характеристик.
Lean-QIT предлагает машиночитаемую основу для формальной QIT и служит композируемой информационной подложкой для ИИ-ассистированной формализации, автоматического поиска доказательств и агентного рассуждения.