Les auteurs présentent LeanQIT, une bibliothèque Lean 4 conçue pour fournir une couche opérationnelle réutilisable pour la théorie de l'information quantique (QIT) à dimension finie. Cette infrastructure définit les codes, les critères d'erreur, les taux atteignables et les capacités indépendamment de leurs caractérisations informationnelles.
- Fournit des interfaces composables et vérifiées par le noyau pour les états quantiques, les canaux, les codes sources et canaux, et le test d'hypothèses.
- Formalise le théorème de codage source quantique de Schumacher, le théorème de capacité classique de Holevo--Schumacher--Westmoreland, et le théorème de capacité classique assistée par intrication avec sa forte réciproque.
- Expose des composants réutilisables d'atteignabilité, de réciproque et asymptotiques pour séparer les définitions opérationnelles des caractérisations analytiques.
Lean-QIT offre un fondement lisible par machine pour la QIT formelle et sert de substrat de connaissances compositionnel pour la formalisation assistée par IA, la recherche automatique de preuves et le raisonnement agentique.