Os autores apresentam o LeanQIT, uma biblioteca Lean 4 projetada para fornecer uma camada operacional reutilizável para a teoria da informação quântica (QIT) de dimensão finita. Essa infraestrutura define códigos, critérios de erro, taxas alcançáveis e capacidades independentemente de suas caracterizações teórico-informacionais.
- Fornece interfaces composáveis verificadas pelo kernel para estados quânticos, canais, códigos de fonte e canal, e teste de hipóteses.
- Formaliza o teorema de codificação de fonte quântica de Schumacher, o teorema de capacidade clássica de Holevo--Schumacher--Westmoreland e o teorema de capacidade clássica assistida por emaranhamento com sua forte recíproca.
- Expõe componentes reutilizáveis de alcançabilidade, recíproco e assintóticos para separar definições operacionais de caracterizações analíticas.
O Lean-QIT oferece uma base legível por máquina para QIT formal e serve como substrato de conhecimento composicional para formalização assistida por IA, busca automática de provas e raciocínio agêntico.