Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Collections

The Quantum Formalization Drive

A coordinated effort to formalize the mathematics of quantum information and quantum computation in Lean 4.

Scope: missions in quantum information theory, quantum computation and algorithms, quantum complexity theory, quantum error correction, entanglement theory, and quantum learning.

1230 missions

Missions

551–575 of 1230
Open836Completed394All1230
Quantum Information·Captain: Gohan

Remarks on additivity of the Holevo channel capacity and of the entanglement of formationResearch Paper

The purpose of these notes is to discuss the relation between the additivity questions regarding the quantities (Holevo) capacity of a quantum channel T and entanglement of formation of a given bipartite state. In particular, using the Stinespring dilation theorem, we give a formula for the channel capacity involving entanglement of formation. This can be…

22 thms2 active usersReviewed
🏆Completed
Quantum Information·Captain: Gohan

G-gerbes, principal 2-group bundles and characteristic classesResearch Paper

Let GGG be a Lie group and G→\Aut(G)G\to\Aut(G)G→\Aut(G) be the canonical group homomorphism induced by the adjoint action of a group on itself. We give an explicit description of a 1-1 correspondence between Morita equivalence classes of, on the one hand, principal 2-group [G→\Aut(G)][G\to\Aut(G)][G→\Aut(G)]-bundles over Lie groupoids and, on the other hand, GGG-extensions of Lie groupoids (i.e.\…

2 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Some remarks on port-based teleportationResearch Paper

Port-based teleportation (PBT) is a teleportation scheme such that the teleported state appears in one of receiver's multiple output ports without any correcting operation on the output port. In this paper, we make some remarks on PBT. Those include the possibility of recoverable PBT (a hybrid protocol between PBT and the standard teleportation scheme), the…

19 thms2 active usersReviewed
Quantum Information·Captain: Gohan

An Infinite Sequence of Additive Channels: the Classical Capacity of Cloning ChannelsResearch Paper

We introduce an infinite sequence of quantum channels for which the Holevo capacity is additive. The channel series is closely related to the quantum channels arising from universal quantum cloning machines. The additivity proof is motivated by a special property the studied channels enjoy: the property of conjugate degradability. As a consequence of the…

15 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Gaussian relative entropy of entanglementResearch Paper

For two gaussian states with given correlation matrices, in order that relative entropy between them is practically calculable, I in this paper describe the ways of transforming the correlation matrix to matrix in the exponential density operator. Gaussian relative entropy of entanglement is proposed as the minimal relative entropy of the gaussian state…

20 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Entanglement Measures and Purification ProceduresResearch Paper

We generalize previously proposed conditions each measure of entanglement has to satisfy. We present a class of entanglement measures that satisfy these conditions and show that the Quantum Relative Entropy and Bures Metric generate two measures of this class. We calculate the measures of entanglement for a number of mixed two spin 1/2 systems using the…

32 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Equivalences of Smooth and Continuous Principal Bundles with Infinite-Dimensional Structure GroupResearch Paper

Let K be a a Lie group, modeled on a locally convex space, and M a finite-dimensional paracompact manifold with corners. We show that each continuous principal K-bundle over M is continuously equivalent to a smooth one and that two smooth principal K-bundles over M which are continuously equivalent are also smoothly equivalent. In the concluding section, we…

5 thms2 active usersReviewed
🏆Completed
Quantum Information·Captain: Gohan

Higher gauge theory I: 2-BundlesResearch Paper

I categorify the definition of fibre bundle, replacing smooth manifolds with differentiable categories, Lie groups with coherent Lie 2-groups, and bundles with a suitable notion of 2-bundle. To link this with previous work, I show that certain 2-categories of principal 2-bundles are equivalent to certain 2-categories of (nonabelian) gerbes. This…

7 thms2 active usersReviewed
🏆Completed
Quantum Information·Captain: Gohan

Derived Algebraic Geometry II: Noncommutative AlgebraResearch Paper

In this paper, we present an infinity-categorical version of the theory of monoidal categories. We show that the infinity category of spectra admits an essentially unique monoidal structure (such that the tensor product preserves colimits in each variable), and thereby recover the classical smash-product operation on spectra. We develop a general theory of…

2 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Bounded functional calculi for unbounded operatorsResearch Paper

This article summarises the theory of several bounded functional calculi for unbounded operators that have recently been discovered. The extend the Hille--Phillips calculus for (negative) generators AAA of certain bounded C0C_0C0​-semigroups, in particular for bounded semigroups on Hilbert spaces and bounded holomorphic semigroups on Banach spaces. They include…

37 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Low dimensional bound entanglement with one-way distillable cryptographic keyResearch Paper

We provide a class of bound entangled states that have positive distillable secure key rate. The smallest state of this kind is 4⊗44 \otimes 44⊗4, which shows that peculiar security contained in bound entangled states does not need high dimensional systems. We show, that for these states a positive key rate can be obtained by {\it one-way} Devetak-Winter…

19 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Computing Stabilized Norms for Quantum Operations via the Theory of Completely Bounded MapsResearch Paper

The diamond and completely bounded norms for linear maps play an increasingly important role in quantum information science, providing fundamental stabilized distance measures for differences of quantum operations. Based on the theory of completely bounded maps, we formulate an algorithm to compute the norm of an arbitrary linear map. We present an…

14 thms2 active usersReviewed
Quantum Information·Captain: Gohan

The Quantum State of a Propagating Laser FieldResearch Paper

Optical implementations of quantum communication protocols typically involve laser fields. However, the standard description of the quantum state of a laser field is surprisingly insufficient to understand the quantum nature of such implementations. In this paper, we give a quantum information-theoretic description of a propagating continuous-wave laser…

13 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Affine and degenerate affine BMW algebras: The centerResearch Paper

The degenerate affine and affine BMW algebras arise naturally in the context of Schur-Weyl duality for orthogonal and symplectic Lie algebras and quantum groups, respectively. Cyclotomic BMW algebras, affine Hecke algebras, cyclotomic Hecke algebras, and their degenerate versions are quotients. In this paper the theory is unified by treating the orthogonal…

14 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Degrees of concealment and bindingness in quantum bit commitment protocolsResearch Paper

Although it is impossible for a bit commitment protocol to be both arbitrarily concealing and arbitrarily binding, it is possible for it to be both partially concealing and partially binding. This means that Bob cannot, prior to the beginning of the unveiling phase, find out everything about the bit committed, and Alice cannot, through actions taken after…

7 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Integrability of unitary representations on reproducing kernel spacesResearch Paper

Let g be a Banach Lie algebra and τ: g ---> g an involution. Write g=h+q for the eigenspace decomposition of g with respect to τand g^c := h+iq for the dual Lie algebra. In this article we show the integrability of two types of infinitesimally unitary representations of g^c. The first class of representation is determined by a smooth positive definite…

8 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Multiplicativity of completely bounded ppp-norms implies a strong converse for entanglement-assisted capacityResearch Paper

The fully quantum reverse Shannon theorem establishes the optimal rate of noiseless classical communication required for simulating the action of many instances of a noisy quantum channel on an arbitrary input state, while also allowing for an arbitrary amount of shared entanglement of an arbitrary form. Turning this theorem around establishes a strong…

24 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Achievable rates for the Gaussian quantum channelResearch Paper

We study the properties of quantum stabilizer codes that embed a finite-dimensional protected code space in an infinite-dimensional Hilbert space. The stabilizer group of such a code is associated with a symplectically integral lattice in the phase space of 2N canonical variables. From the existence of symplectically integral lattices with suitable…

11 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Exact synthesis of single-qubit unitaries over Clifford-cyclotomic gate setsResearch Paper

We generalize an efficient exact synthesis algorithm for single-qubit unitaries over the Clifford+T gate set which was presented by Kliuchnikov, Maslov and Mosca. Their algorithm takes as input an exactly synthesizable single-qubit unitary--one which can be expressed without error as a product of Clifford and T gates--and outputs a sequence of gates which…

18 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Secure quantum key distribution with an uncharacterized sourceResearch Paper

We prove the security of the Bennett-Brassard (BB84) quantum key distribution protocol for an arbitrary source whose averaged states are basis-independent, a condition that is automatically satisfied if the source is suitably designed. The proof is based on the observation that, to an adversary, the key extraction process is equivalent to a measurement in…

11 thms2 active usersReviewed
Quantum Information·Captain: Gohan

fff-divergence InequalitiesResearch Paper

This paper develops systematic approaches to obtain fff-divergence inequalities, dealing with pairs of probability measures defined on arbitrary alphabets. Functional domination is one such approach, where special emphasis is placed on finding the best possible constant upper bounding a ratio of fff-divergences. Another approach used for the derivation of…

67 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Correlation measures of a quantum state and information characteristics of a quantum channelResearch Paper

We discuss the interconnections between basic correlation measures of a bipartite quantum state and basic information characteristics of a quantum channel, focusing on the benefits of these interconnections for solving specific problems concerning the characteristics of both types. We describe properties of the (unoptimized and optimized) quantum discord in…

65 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Quantum Feedback ChannelsResearch Paper

In Shannon information theory the capacity of a memoryless communication channel cannot be increased by the use of feedback. In quantum information theory the no-cloning theorem means that noiseless copying and feedback of quantum information cannot be achieved. In this paper, quantum feedback is defined as the unlimited use of a noiseless quantum channel…

10 thms2 active usersReviewed
Quantum Information·Captain: Gohan

Non-integral central extensions of loop groupsResearch Paper

It is well-known that the central extensions of the loop group of a compact, simple and 1-connected Lie group are parametrised by their level k∈Zk \in Zk∈Z. This article concerns the question how much can be said for arbitrary k∈Rk \in Rk∈R and we show that for each kkk there exists a Lie groupoid which has the level kkk central extension as its quotient if k∈Zk \in Zk∈Z. By…

6 thms2 active usersReviewed
Quantum Information·Captain: Gohan

On completion of the cone of CP linear maps with respect to the energy-constrained diamond normResearch Paper

For a given positive operator GGG we consider the cones of linear maps between Banach spaces of trace class operators characterized by the Stinespring-like representation with G\sqrt{G}G​-bounded and G\sqrt{G}G​-infinitesimal operators correspondingly. We prove the completeness of both cones w.r.t. the energy-constrained diamond norm induced by GGG (as an energy…

4 thms2 active usersReviewed
PreviousPage 23 of 50Next

Top contributors

RankContributorAccepted solutionsSubmitted problems
1FIfizzyinc3287472
2SHshivm41212
3MAMazecto256251
4MAmarwahaha144197
5NINickrobbins9514247
6KMkmehltretter821385
7ECEthan Cheung Wang1370
8MRMrnaiq9219
9ALAlien608689
10MRmrfancypants760

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me