लेखक LeanQIT प्रस्तुत करते हैं, जो एक Lean 4 लाइब्रेरी है जिसे परिमित-आयामी क्वांटम सूचना सिद्धांत (QIT) के लिए पुनः उपयोग योग्य संचालन परत प्रदान करने के लिए डिज़ाइन किया गया है। यह बुनियादी ढांचा अपनी सूचना-सैद्धांतिक विशेषताओं से स्वतंत्र रूप से कोड, त्रुटि मानदंड, प्राप्त दरों और क्षमताओं को परिभाषित करता है।
- क्वांटम अवस्थाओं, चैनलों, स्रोत और चैनल कोड, और परिकल्पना परीक्षण के लिए संयोजनीय, kernel-जाँचे इंटरफेस प्रदान करता है।
- Schumacher के क्वांटम स्रोत-कोडिंग प्रमेय, Holevo--Schumacher--Westmoreland क्लासिकल-क्षमता प्रमेय, और इसके प्रबल विपरीत के साथ entanglement-assisted क्लासिकल-क्षमता प्रमेय को औपचारिक बनाता है।
- संचालन परिभाषाओं को विश्लेषणात्मक विशेषताओं से अलग करने के लिए पुनः उपयोग योग्य प्राप्तियता, विपरीत और asymptotic घटकों को उजागर करता है।
Lean-QIT औपचारिक QIT के लिए मशीन-पठनीय आधार प्रदान करता है और AI-सहायक औपचारिकीकरण, स्वचलित प्रमाण खोज, और एजेंटिक तर्क के लिए संयोजनी ज्ञान आधारभूत के रूप में कार्य करता है।