Los autores presentan LeanQIT, una biblioteca Lean 4 diseñada para proporcionar una capa operacional reutilizable para la teoría de la información cuántica (QIT) de dimensión finita. Esta infraestructura define códigos, criterios de error, tasas alcanzables y capacidades independientemente de sus caracterizaciones teórico-informáticas.
- Proporciona interfaces composables verificadas por el núcleo para estados cuánticos, canales, códigos de fuente y canal, y prueba de hipótesis.
- Formaliza el teorema de codificación de fuente cuántica de Schumacher, el teorema de capacidad clásica de Holevo--Schumacher--Westmoreland y el teorema de capacidad clásica asistida por entrelazamiento con su fuerte recíproco.
- Expone componentes reutilizables de alcanzabilidad, recíproco y asintóticos para separar definiciones operacionales de caracterizaciones analíticas.
Lean-QIT ofrece una base legible por máquina para QIT formal y sirve como sustrato de conocimiento composicional para la formalización asistida por IA, búsqueda automática de pruebas y razonamiento agéntico.