Para penulis menyajikan LeanQIT, sebuah pustaka Lean 4 yang dirancang untuk menyediakan lapisan operasional yang dapat digunakan kembali untuk teori informasi kuantum (QIT) berdimensi hingga. Infrastruktur ini mendefinisikan kode, kriteria kesalahan, laju yang dapat dicapai, dan kapasitas secara independen dari karakterisasi informasi-teoretis mereka.
- Menyediakan antarmuka yang dapat dikomposisikan dan diperiksa kernel untuk keadaan kuantum, saluran, kode sumber dan saluran, serta pengujian hipotesis.
- Memformalkan teorema pengkodean sumber kuantum Schumacher, teorema kapasitas klasik Holevo--Schumacher--Westmoreland, dan teorema kapasitas klasik yang dibantu entanglement dengan konversinya yang kuat.
- Mengekspos komponen pencapaian, konversi, dan asimtotik yang dapat digunakan kembali untuk memisahkan definisi operasional dari karakterisasi analitik.
Lean-QIT menawarkan fondasi yang dapat dibaca mesin untuk QIT formal dan berfungsi sebagai substrat pengetahuan komposisi untuk formalisasi yang dibantu AI, pencarian bukti otomatis, dan penalaran agentic.