lean-quantum

Lean formalization of quantum information theory and quantum computation.

Visitors from the IBIS 2026 poster: the formalization presented there (from the theorems of Löwner and Hiai–Petz to the generalized quantum Stein's lemma) is on the paper2 branch.

Updates

• 2026-10. The formalization reported in the second Lean-Quantum paper (Paper 2, in preparation for submission) is available on the paper2 branch.
• 2026-10. The code was updated to accompany version 2 of arXiv:2607.05492 (to be submitted). It adopts several of Mathlib's values, the principles of the standard mathematical library, for example by splitting large files into smaller ones organized by topic and by renaming declarations to follow the Mathlib naming conventions, with a few exceptions. Some definitions and theorems were also restated. The 34 theorems listed in Results can now be checked independently with Comparator. The code accompanying arXiv v1 remains available at commit bf1c4f6.

Contents

• What is covered
• Linear and bounded linear operators
• How to run
• Independent proof checking
• Results
• Poster presentation (AQIS 2026)
• How to cite

What is covered

The library currently provides foundations mainly for finite-dimensional quantum information theory (some operator inequalities also in infinite dimension), checked by Lean's kernel (the small core of Lean that checks proofs), including:

• quantum systems, states, and completely positive trace-preserving (CPTP) maps;
• partial traces on tensor-product spaces, Choi operators, Kraus representations, and Stinespring representations;
• operator monotonicity and convexity, the Löwner–Heinz theorem, Jensen's operator inequality, generalized perspectives, operator geometric means, Hilbert-Schmidt operator spaces, and Lieb-Ando trace inequalities;
• sandwiched Renyi relative entropy and its data-processing inequality (DPI), together with non-negativity and its limits to Umegaki and max-relative entropy;
• von Neumann entropy, the DPI for Umegaki relative entropy, and strong subadditivity; and
• supporting lemmas on the continuous functional calculus (such as powers of tensor products and derivatives of powers in the exponent), trace Young inequalities, and averages over the Haar measure on unitary groups.

The module Quantum.lean imports every module (Lean file) in the Quantum/ directory, so import Quantum makes all public declarations of the library available.

Linear and bounded linear operators

On a finite-dimensional Hilbert space every linear operator is bounded, so the linear operators and the bounded linear operators can be identified. In Lean, however, they are different types (ℋ →ₗ[ℂ] ℋ and ℋ →L[ℂ] ℋ). Mathlib treats as a C*-algebra, on which the continuous functional calculus cfc (used to define operator powers and logarithms) and Haar measure on unitary groups are available. This repository also equips with the C*-algebra structure transferred from , and the proofs move operators to where these tools are needed; the Hilbert–Schmidt inner product is also built on it. By definition, cfc returns on elements that do not satisfy its precondition (for real functions, non-self-adjoint elements); the table of Definitions used in the theorems therefore also gives values outside the intended inputs. The main finite-dimensional theorems (on complete positivity, Lieb–Ando, entropies and the DPI, among others) are stated for . The theorems on operator powers are stated in general C*-algebras. Those on Jensen's operator inequality and generalized perspectives are stated for on Hilbert spaces of any dimension, including infinite dimension.

How to run

These steps compile and check the code on your own computer; they are not needed for reading this README. If Lean is not installed, first install it with elan.

git clone https://github.com/Hayata-Yamasaki-Group/lean-quantum.git
cd lean-quantum
lake exe cache get   # download the prebuilt files of Mathlib
lake build           # check every proof with Lean's kernel

• The Lean version and the dependencies are fixed by lean-toolchain and lake-manifest.json; the only mathematics library dependency is Mathlib (Comparator is a verification tool).
• Do not run lake update (it would change the pinned versions of the dependencies).
• lake build succeeds even with sorry, which only produces a warning. The library and the solution file contain no sorry (the statements-only file uses it on purpose as a placeholder for omitted proofs); the axioms a theorem depends on can be checked with #print axioms followed by its name (a proof using sorry shows sorryAx).

Independent proof checking

Guarantee: Comparator lets the user conclude, without trusting the whole codebase but only the statements-only file Paper1.lean (the challenge, in Comparator's terms), the modules it imports, the check configuration (Paper1.json), and the build configuration (lakefile), that, when the check succeeds, the 34 theorems stated in Paper1.lean (listed under Results) are proved (see the Comparator README for its other assumptions).

How it checks: It builds the solution file Paper1Solution.lean (the solution, in Comparator's terms) in a sandbox (landrun) that restricts where it can write, checks that each theorem has the same statement as in Paper1.lean (including the definitions the statement uses) and uses only Lean's three standard axioms (propext, Classical.choice, Quot.sound; a proof using sorry fails here), and rechecks the proofs with both Lean's kernel and the independent nanoda kernel.

What is trusted: For the imported modules, the user needs to trust only the meaning of the terms they define (checked with the table of Definitions used in the theorems) and that they contain no program that alters what is checked or how it is checked when the files are built (Lean files can run programs during the build), because Comparator also rechecks the proofs in those modules that the 34 theorems depend on.

Run: For this version, Comparator was run on Linux with Landlock enabled, building the solution file in the sandbox, and all 34 theorems were accepted by both Lean's kernel and nanoda.

What it cannot check: Comparator cannot check whether the statements of the Lean theorems (including implicit arguments and type-class instances), and the definitions they use, state what the paper intends; this has to be checked by the user, for which the definitions are listed below in a table under Definitions used in the theorems. See ComparatorChallenges/README.md for setup and execution instructions (running it isolated requires Linux with Landlock enabled).

Results

The 34 theorems, chosen as the targets of the Comparator check rather than all theorems of the library, are shown in the tables of the following subsections.

1. Complete positivity and channel representations (6)
2. Operator monotone and convex powers (5)
3. Jensen's operator inequality and generalized perspectives (6)
4. Lieb–Ando trace inequalities (3)
5. Sandwiched Rényi data processing and consequences (9)
6. Diagnostic results (5)

• Definitions used in the theorems

The tables in subsections 1–6 below have the following three columns.

• Paper location
  • In subsections 1–5, a link to the equation or the passage of the text (not the Lean code listed in the paper) where our paper (arXiv:2607.05492) refers to the theorem
  • In subsection 6, a link to the section where the paper introduces predicates such as operator convexity
  • Passages of the text are quoted before each table by their first and last words joined by “…”
  • Until version 2 is public, locations give the arXiv v1 sections, equation numbers and text and link to arXiv v1 (we plan to replace them with those of version 2 once it appears)
• Statement
  • In subsections 1–5, the mathematical theorem taken up by version 2 of the paper (to be submitted); most have original sources, which, together with their proofs, are the basis of the formalization
  • Where the assumptions or scope differ from the original sources or the paper in order to state the theorem in Lean, this is said in this column of each table and in the text of the subsection
• Lean declaration
  • The formalization of the theorem in Lean
  • The link opens the declaration in the statements-only file Paper1.lean
  • The proof can be followed from the theorem of the same name in Paper1Solution.lean

The user compares each Statement with the Lean statement of its Lean declaration, and, where the Lean statement uses definitions of this repository, also with the table of Definitions used in the theorems. The user checks that the Lean statement (including implicit arguments and type-class instances) is the intended formalization; that it is proved is checked by Comparator (see Independent proof checking for what Comparator relies on).

Of the 34 theorems, 29 formalize some of the theorems stated in Sections 1.5 and 2–4 of the paper, sometimes splitting one theorem into several Lean theorems. The other five show the grounds on which we defined operator convexity and concavity only for self-adjoint elements (6. Diagnostic results) and are not theorems of the paper. Each subsection first shows one of its theorems as an example, states the assumptions common to the subsection, and lists its theorems in the table. Below, PSD means that an operator (in subsection 2, an element of a C*-algebra) is positive semidefinite, and PD that it is positive semidefinite and invertible.

1. Complete positivity and channel representations

CP is complete positivity in the sense of Mathlib (IsCompletelyPositive in Definitions used in the theorems). Choose a basis of the input space (not necessarily orthonormal) and set ; the characterization by the Choi operator (Choi's theorem) then reads:

The theorems in this subsection concern complex-linear maps between the operator spaces of finite-dimensional complex Hilbert spaces (also called superoperators). The paper states the following six equivalences together in one paragraph of Section 2.2.

Quoted paper locations:

• Section 2.2: “The main equivalence theorem relates … rank Stinespring representations.”

Paper location	Statement	Lean declaration
Section 2.2	iff is positive.	cp_iff_tensor
Same as above	iff the Choi operator .	cp_iff_choi
Same as above	iff for finite .	cp_iff_kraus
Same as above	iff for some Kraus representation.	cp_iff_rank_kraus
Same as above	iff for finite-dimensional .	cp_iff_stinespring
Same as above	iff for some Stinespring representation.	cp_iff_rank_stinespring

2. Operator monotone and convex powers

For elements of an ordered complex C*-algebra and a real number , the Löwner–Heinz inequality reads:

The theorems in this subsection concern elements of an ordered complex C*-algebra; real powers are defined by the continuous functional calculus (on PSD elements for nonnegative powers and PD elements for negative powers).

Quoted paper locations:

• Section 3.1 (positive powers): “These express the standard facts that … for .”
• Section 3.1 (negative powers): “The current Core interface also includes negative-power results, … trace inequalities:”

Paper location	Statement	Lean declaration
Section 3.1 (positive powers)	is operator monotone on for .	power_Icc_zero_one_operatorMonotoneOn_Ici
Same as above	is operator concave on for .	operatorConcaveOn_rpow_Ici
Same as above	is operator convex on for .	operatorConvexOn_rpow_Ici
Section 3.1 (negative powers)	is operator monotone on for .	power_Icc_neg_one_zero_neg_operatorMonotoneOn_Ioi
Same as above	is operator concave on for .	operatorConcaveOn_neg_rpow_Ioi

3. Jensen's operator inequality and generalized perspectives

Jensen's operator inequality for finitely many operators reads as follows: for bounded operators on a complex Hilbert space (finitely many ) with PSD and , and a real function uniformly operator convex on (operator convex on every complex Hilbert space), continuous, with ,

The theorems in this subsection use complex Hilbert spaces without a finite-dimensional assumption.

Quoted paper locations:

• Section 3.4: “The main theorem packages the implication … two-operator Jensen form:”
• Section 3.5 (convexity): “Thus, if is operator convex … positive-definite domains.”
• Section 3.5 (concavity): “The corresponding concavity theorem is obtained … to :”

Paper location	Statement	Lean declaration
Section 3.4	The two-operator Jensen inequality holds for PSD inputs with a contractive column, that is, .	jensenColumn_of_opConvexIciAll
Section 3.5 (convexity)	The generalized perspective is jointly convex for PSD and PD ; is uniformly operator convex and continuous on with , and is operator concave, continuous and positive on .	jointlyConvexOn_generalizedPerspective_psdSet_pdSet
Section 3.5 (concavity)	The generalized perspective is jointly concave for PSD and PD ; is uniformly operator concave and continuous on with , and is as in the convexity row.	jointlyConcaveOn_generalizedPerspective_psdSet_pdSet
Section 3.4, Eq. (30)	The finite Jensen inequality holds for uniformly operator convex and continuous on with .	jensenFinite_of_opConvexIciAll
Same as above	The finite Jensen inequality holds for self-adjoint with spectra in an open interval containing zero (not necessarily PSD) and uniformly operator convex on with .	jensenFinite_of_opConvexOnAll_of_isOpen
Same as above	The finite Jensen inequality holds for self-adjoint with spectra in an interval containing zero and uniformly operator convex on with and continuity from within at included endpoints.	jensenFinite_of_opConvexOnAll_of_endpoints

4. Lieb–Ando trace inequalities

For operators on a finite-dimensional complex Hilbert space with PD, and , the following real-valued Lieb functional is jointly concave (Lieb's concavity theorem):

The theorems in this subsection use finite-dimensional complex Hilbert spaces.

Paper location	Statement	Lean declaration
Section 3.7, Eq. (39)	The Lieb functional is jointly concave for .	jointlyConcaveOn_liebTraceMap_pdSetLM
Same as above	The Lieb functional is jointly convex for .	jointlyConvexOn_liebTraceMap_pdSetLM
Section 3.7, Eq. (40)	is jointly convex for , , .	jointlyConvexOn_andoTraceMap_pdSetLM

5. Sandwiched Rényi data processing and consequences

Theorem 1 is the data-processing inequality (DPI) for the sandwiched Rényi relative entropy: for density operators on ( PD), a CPTP map , and ,

The two tripartite strong subadditivity (SSA) rows state with . The theorems in this subsection use finite-dimensional complex Hilbert spaces. All DPI maps are CPTP, and the DPI and Rényi SSA statements use the range of stated above. Divergences are real-valued, except that the NN versions are the extended-real-valued versions for PSD inputs (Theorem 1 is stated with the NN version).

Quoted paper locations:

• Section 4.4: “The development also formalizes … DPI for positive semidefinite operators.”
• Section 1.5: “In the limit , the sandwiched Rényi … Umegaki relative entropy”

Paper location	Statement	Lean declaration
Section 4.4	The real-valued DPI holds for PD inputs and outputs (the core of the proof of Theorem 1).	sandwichedRenyiDiv_monotone
Section 4.4	The extended-real DPI holds for arbitrary PSD inputs.	sandwichedRenyiDivNN_monotone
Section 4.4, Eq. (65), Theorem 1	The DPI holds for density inputs with positive definite (Theorem 1).	sandwichedRenyiDivNN_monotone_of_isDensity
Section 1.5, Eq. (4)	holds for states.	strongSubadditivity_of_state
Section 1.5	For PD inputs, the sandwiched Rényi relative entropy converges as to the Umegaki relative entropy divided by .	tendsto_sandwichedRenyiDiv_umegakiNorm_right
Same as above	For PD inputs, the sandwiched Rényi relative entropy converges as , , to the Umegaki relative entropy divided by .	tendsto_sandwichedRenyiDiv_umegakiNorm_of_pd
Section 1.5, Eq. (3)	The extended-real tripartite SSA holds for arbitrary PSD input.	sandwichedRenyiDivNN_tripartiteSSA
Same as above	The real-valued tripartite SSA holds when is PD and on both sides and are nonzero.	sandwichedRenyiDiv_tripartiteSSA
Section 1.5	For PSD inputs with and , the sandwiched Rényi relative entropy converges as , , to the Umegaki relative entropy divided by .	tendsto_sandwichedRenyiDiv_umegakiNorm_of_supportLE

6. Diagnostic results

The five theorems in this subsection show the grounds on which we defined operator convexity and concavity only for self-adjoint elements, and are not theorems asserted by the paper. OperatorConvex and OperatorConcave are predicates quantified over all elements of a complex C*-algebra, including non-self-adjoint ones, and OperatorConvexAll and OperatorConcaveAll impose them on every complete, nontrivial complex Hilbert space; by definition, cfc returns on non-self-adjoint elements, so only satisfies them (for a nontrivial C*-algebra):

Hence, with these predicates as hypotheses, the hypothesis fails for and the theorem holds only vacuously. The theorems on Jensen's operator inequality and generalized perspectives therefore use predicates that quantify only over self-adjoint elements with spectrum in an interval (such as OperatorConvexOn); for example, operator convexity restricted to (PSD elements) admits . The paper locations below point to Section 3.1, where the paper introduces predicates such as operator convexity.

Paper location	Statement	Lean declaration
Section 3.1	OperatorConvex forces for every real .	OperatorConvex.eq_zero_of_nontrivial
Same as above	OperatorConcave forces for every real .	OperatorConcave.eq_zero_of_nontrivial
Same as above	OperatorConvexAll forces .	OperatorConvexAll.eq_zero
Same as above	OperatorConcaveAll forces .	OperatorConcaveAll.eq_zero
Same as above	is uniformly operator convex on .	operatorConvexOnAll_Ici_sq

Definitions used in the theorems

The table below explains, in the order in which the subsections of the results mention them, the definitions that appear in the statements of the 34 theorems of Paper1.lean; definitions from Mathlib are not listed. Each entry states what the Lean definition says, including its value outside the intended inputs.

Lean definition	What the definition says
Common
Qudit	Type class for a finite-dimensional complex inner-product space (normed and complete). Dimension is allowed; nonzero dimension is the separate assumption Nontrivial
L	The type L ℋ of complex-linear maps ℋ →ₗ[ℂ] ℋ. Its order is Mathlib's Löwner order: iff is positive semidefinite
B	The type B ℋ of bounded (continuous) complex-linear operators ℋ →L[ℂ] ℋ, with the Löwner order
Tr	The trace LinearMap.trace ℂ ℋ on L ℋ, complex-valued
T	The type T ℋ₁ ℋ₂ of complex-linear maps L ℋ₁ →ₗ[ℂ] L ℋ₂, with no positivity or trace condition
1. Complete positivity and channel representations
IsCompletelyPositive	is completely positive in Mathlib's sense (CompletelyPositiveMap): for every , applying entrywise sends each positive matrix over the C*-algebra L ℋ₁ to a positive matrix
AmplificationPositive	, from to , sends positive semidefinite operators to positive semidefinite operators
ChoiPositive	For a basis of (not necessarily orthonormal), in , where
HasKraus	There are a finite index type (possibly empty, in the universe of ) and linear maps with for all
HasRankKraus	HasKraus with, in addition, equal to choiRank b Φ (below)
traceOutRight	Partial trace over the right factor: the linear map with (defined as traceOutLeft (below) after swapping the factors)
choiRank	The rank (dimension of the range) of the Choi operator of ChoiPositive, a natural number
2. Operator monotone and convex powers
OperatorMonotoneOn	In a fixed ordered C*-algebra: for all self-adjoint with spectra in and , , where is Mathlib's continuous functional calculus cfc f A
LownerHeinzCore.OperatorConcaveOn	OperatorConvexOn s (-f) (below) in the same algebra
OperatorConvexOn	In a fixed ordered C*-algebra: for all self-adjoint with spectra in and , (cfc); the spectrum of is not separately constrained
3. Jensen's operator inequality and generalized perspectives
OperatorConvexIciAllContNonposAtZero	OperatorConvexOnAll (Set.Ici 0) f (below), continuity of on , and
JensenContractiveColumnCondition	On a fixed Hilbert space: for self-adjoint in B ℋ with spectra in and all with , (cfcR, below)
LownerHeinzTheorem.OperatorConcaveOn	LownerHeinzCore.OperatorConcaveOn s f in the C*-algebra B ℋ of the given Hilbert space
JointlyConvexOn	For , and , with and , is at most ; need not be convex
psdSet	The set of self-adjoint in B ℋ with spectrum in
pdSet	The set of self-adjoint in B ℋ with spectrum in (positive semidefinite and invertible)
generalizedPerspective	with = cfcR (fun x ↦ h x ^ (±1/2)) B (cfcR below); defined for all , and positivity and invertibility of are assumed in the theorems
OperatorConcaveOnAll	LownerHeinzTheorem.OperatorConcaveOn s f on every nontrivial complete complex Hilbert space in universe u, of any dimension
JointlyConcaveOn	JointlyConvexOn with the inequality reversed
cfcR	cfcR f A is Mathlib's cfc f A for in B ℋ (real functional calculus ); it is if is not self-adjoint or is not continuous on its spectrum
OperatorConvexOnAll	LownerHeinzCore.OperatorConvexOn s f in B K for every nontrivial complete complex Hilbert space in universe u, of any dimension
4. Lieb–Ando trace inequalities
pdSetLM	The set of in L ℋ whose bounded version lies in pdSet: self-adjoint with spectrum in , that is, positive definite
liebTraceMap	liebTraceMap s K A B , with Mathlib's real powers CFC.rpow ( on arguments that are not positive semidefinite)
andoTraceMap	andoTraceMap q r K A B , with the same powers
5. Sandwiched Rényi data processing and consequences
CPTP	Structure: a completely positive map L ℋ₁ → L ℋ₂ (Mathlib's CompletelyPositiveMap) with for all ; Φ.toFun is the map
sandwichedRenyiDiv	Real-valued with = sandwichedQuasi (below); Lean's Real.log has , no support condition is imposed, and the value at is
sandwichedRenyiDivNN	Extended-real: if and SupportLE ρ σ (below) fails, or if , and ; otherwise sandwichedRenyiDiv α ρ σ. In particular
IsDensity	is positive semidefinite (IsPositive) and
IsPositiveDefinite	is positive semidefinite and
vonNeumannEntropy	, with Mathlib's CFC.log (cfc Real.log, so on the kernel); defined for every operator
traceOutLeft	Partial trace over the left factor: the linear map with
traceOutThird	From to : regroup by the associator, then apply traceOutRight ()
umegakiNorm	Real-valued divided by , with CFC.log; no support condition is imposed
tripartiteReference	tripartiteReference X Y is moved to by the associator
sandwichedQuasi	with and powers by CFC.rpow (for positive semidefinite , a negative power is taken on the support and is on the kernel)
SupportLE	(for self-adjoint , this is )
6. Diagnostic results
OperatorConvex	For all in a fixed ordered C*-algebra, not necessarily self-adjoint, and , with cfc ( on elements that are not self-adjoint)
OperatorConcave	OperatorConvex (-f)
OperatorConvexAll	OperatorConvex f in B K for every nontrivial complete complex Hilbert space in universe u
OperatorConcaveAll	OperatorConcave f in B K for every nontrivial complete complex Hilbert space in universe u

Poster presentation (AQIS 2026)

Click the thumbnail to view the poster presented at AQIS 2026.

This presentation is preserved as published and includes plans, examples, and build statistics of our development branch (not public) at that time. For the scope of this repository, see What is covered.

How to cite

If you use this library, please cite the accompanying paper:

@article{kasaura2026leanquantum,
  title         = {Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information},
  author        = {Kasaura, Kazumi and Tsukamoto, Kei and Mori, Kento and
                   Mizuno, Lisa and Namatame, Takahiro and Oriike, Yuta and
                   Taniguchi, Masaya and Sonoda, Sho and Yamasaki, Hayata},
  year          = {2026},
  eprint        = {2607.05492},
  archivePrefix = {arXiv},
  primaryClass  = {quant-ph},
  doi           = {10.48550/arXiv.2607.05492}
}