يقدم المؤلفون LeanQIT، وهي مكتبة Lean 4 مصممة لتوفير طبقة تشغيلية قابلة لإعادة الاستخدام لنظرية المعلومات الكمية (QIT) ذات الأبعاد المحدودة. تحدد هذه البنية الأساسية الرموز، ومعايير الخطأ، والمعدلات القابلة للتحقيق، والسعات بشكل مستقل عن خصائصها النظرية المعلوماتية.
- توفر واجهات قابلة للتكوين وفحص النواة لحالات الكم، والقنوات، ورموز المصدر والقناة، واختبار الفرضيات.
- تُرسّخ مبرهنة شوماخر لتشفير المصدر الكمي، ومبرهنة سعة هوليفو--شوماخر--ويستموورلاند الكلاسيكية، ومبرهنة السعة الكلاسيكية المساعدة بالتشابك مع عكسها القوي.
- تكشف عن مكونات قابلة لإعادة الاستخدام للتحقيق والعكس والمقاربات لفصل التعاريف التشغيلية عن الخصائص التحليلية.
يوفر Lean-QIT أساسًا قابلًا للقراءة الآلية لـ QIT الرسمي ويعمل كوسط معرفي تجميعي للتشكيل بمساعدة الذكاء الاصطناعي، والبحث التلقائي عن البراهين، والاستدلال الوكي.