Our main focus. This starts by defining quantum states, unitaries and channels. It works up through concepts such as dual maps, pure and separable states, convex combinations, quantum entropies, mutual information, resource theories, and ultimately proving key theorems such as the no-cloning theorem, Choi's theorem on CPTP maps, the data processing inequality, and the generalized quantum Stein's lemma.
This library provides tools for representing numbers with significant figures, performing arithmetic operations while correctly propagating uncertainties, and formatting results for scientific reporting. While Lean lets one work with arbitrary numerical types and prove their properties given semantics of that type, the semantics of uncertainty propagation is not built into Lean's core or Mathlib. This repository gives such appropriate semantics, allowing machine-checkable proofs of computation under the assumptions of an uncertainty model. Several different uncertainty models are supported.
This offers, where possible, computable definitions of real numbered functions, permitted the use of calculation within the type-safety of Lean to check certain proofs involving real numbers. This extends Mathlib's existing construction of real numbers via Cauchy sequences by augmenting it with appropriate computable bounds. This is particularly crucial to scientific computation where messy explicit decimals and numerical checks are frequent.
This project formalizes key concepts and theorems from classical circuit complexity theory, including Boolean circuits and complexity classes (such as NC, AC, and P/poly). Turing machine-based complexity theory is present in Mathlib, but extremely difficult to work with due to the need to "program" the Turing machine. In comparison, the (non-uniform) circuit model is far easier to reason about within Lean. This repository aims to provide a solid foundation for further exploration of complexity theory within Lean. Currently the main target is to complete the proof that NCi ⊆ ACi ⊆ NCi+1, and PARTIY is not in AC0. After this, establishing relationships between classical and quantum complexity classes is a natural next step.