Formalize Open Quantum Problem #24: Secret key from all entangled states

### What is the conjecture

This is problem [#24](https://oqp.iqoqi.oeaw.ac.at/secret-key-from-all-entangled-states) in [Reinhard F. Werner’s collection](https://arxiv.org/abs/quant-ph/0504166), later [collected by a community of quantum researchers](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

> **Problem (Open Quantum Problem #24: “Secret key from all entangled states”).**
> Can all bipartite entangled states be used to generate secret keys?

A standard formalization is via the **distillable secret key** `K_D(ρ_AB)` of a finite-dimensional bipartite state `ρ_AB`:

* `ρ_AB` is **entangled** iff it is not separable, i.e. it cannot be written as
`ρ_AB = ∑_i p_i (α_i ⊗ β_i)`,
where `p_i ≥ 0`, `∑_i p_i = 1`, and `α_i, β_i` are local density operators.
* Let `ψ_ABE` be a purification of `ρ_AB`; the purifying system `E` is held by an eavesdropper Eve.
* For `n` copies, Alice and Bob may apply an `n`-copy **LOPC** protocol
`Λ_n ∈ LOPC(A^n:B^n|E^n → K_n:K'_n|E'_n)`,
built from local quantum operations and public classical communication.
* A rate `R ≥ 0` is **achievable** if there exists a sequence of such protocols with
`|K_n| = |K'_n| = 2^{⌊Rn⌋}` and
`Λ_n(ψ_ABE^{⊗ n}) ≈ (2^{-⌊Rn⌋} ∑_{x=0}^{2^{⌊Rn⌋}-1} |x⟩⟨x|_{K_n} ⊗ |x⟩⟨x|_{K'_n}) ⊗ σ_{E'_n}`
in trace distance as `n → ∞`.
In words: Alice and Bob end with `⌊Rn⌋` almost-perfect shared secret bits that are asymptotically independent of Eve.
* The supremum of achievable rates is the **distillable key** `K_D(ρ_AB)`.

The problem can then be phrased as:

* **Main question / open equivalence problem:** is `K_D(ρ_AB) > 0` for **every** entangled bipartite state `ρ_AB`?
Equivalently, is positivity of distillable key exactly equivalent to entanglement?

Related structure and natural sub-problems:

* Since any distilled EPR pair can be measured to produce a perfect secret bit, positive **distillable entanglement** `E_D(ρ_AB)` implies positive distillable key `K_D(ρ_AB)`.
* It is already known that one does **not** need singlet distillability first: some **bound entangled** states (entangled states with `E_D(ρ_AB)=0`) nevertheless satisfy `K_D(ρ_AB) > 0`.
* Hence the unresolved part is whether there exist **entangled** states with `K_D(ρ_AB)=0`; equivalently, whether secrecy and entanglement are qualitatively the same bipartite resource in the asymptotic setting.
* A particularly natural sharpened question is whether **every bound entangled state**—especially every **PPT-entangled** state—has positive distillable key.
* In the “private state” (`pbit`/`pdit`) formulation, the problem can equivalently be phrased as whether every entangled state can be asymptotically converted into private states at positive rate.
* A related but weaker result says that every entangled state can be mapped by suitable **single-copy measurements** into a classical probability distribution containing secret correlations. The open problem is whether one can always distill an actual secret key at positive asymptotic rate from the quantum state itself.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #24)](https://oqp.iqoqi.oeaw.ac.at/secret-key-from-all-entangled-states)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)
* O. Krüger & R. F. Werner, “Some Open Problems in Quantum Information Theory” (Problem 24):
[https://arxiv.org/abs/quant-ph/0504166](https://arxiv.org/abs/quant-ph/0504166)
[https://arxiv.org/pdf/quant-ph/0504166](https://arxiv.org/pdf/quant-ph/0504166)

Key related references (as listed on the OQP page):

* K. Horodecki, M. Horodecki, P. Horodecki, and J. Oppenheim, “Secure key from bound entanglement” (Phys. Rev. Lett. 94, 160502 (2005); arXiv: quant-ph/0309110)
(shows that some bound entangled states already have positive distillable key)
* I. Devetak and A. Winter, “Distillation of secret key and entanglement from quantum states” (Proc. R. Soc. Lond. A 461, 207–235 (2005); arXiv: quant-ph/0306078)
(gives the fundamental one-way key-distillation / entanglement-distillation framework)
* K. Horodecki, L. Pankowski, M. Horodecki, and P. Horodecki, “Low-dimensional bound entanglement with one-way distillable cryptographic key” (IEEE Trans. Inf. Theory 54, 2621 (2008); arXiv: quant-ph/0506203)
(provides `4×4` bound entangled states with positive key rate, using the Devetak–Winter protocol)
* K. Horodecki, D. Leung, H.-K. Lo, and J. Oppenheim, “Quantum key distribution based on arbitrarily weak distillable entangled states” (Phys. Rev. Lett. 96, 070501 (2006); arXiv: quant-ph/0510067)
(shows secure QKD is possible even when distillable entanglement is arbitrarily small)

Useful additional references for formalization:

* K. Horodecki, M. Horodecki, P. Horodecki, and J. Oppenheim, “General paradigm for distilling classical key from quantum states” (IEEE Trans. Inf. Theory 55, 1898 (2009); arXiv: quant-ph/0506189)
(systematic formulation of distillable key and private states / `pbits`)
* P. Horodecki and R. Augusiak, “Quantum states representing perfectly secure bits are always distillable” (Phys. Rev. A 74, 010302(R) (2006); arXiv: quant-ph/0602176)
(perfect private bits themselves are always distillably entangled)
* A. Acín and N. Gisin, “Quantum correlations and secret bits” (Phys. Rev. Lett. 94, 020501 (2005); arXiv: quant-ph/0310054)
(every entangled state yields secret **correlations** after suitable measurements; related but weaker than positive quantum distillable key)

### Prerequisites needed

* Finite-dimensional quantum mechanics: density matrices, tensor products, purification, partial trace
* Entanglement theory basics: separable vs entangled states, LOCC/LOPC, EPR pairs, distillable entanglement, bound entanglement
* Quantum information / cryptography basics: secret-key distillation, public communication, classical registers, asymptotic rates
* Quantum channels and CPTP maps; local operations and protocols on many copies
* (Useful for the private-state formulation) private states / `pbits`, trace distance, asymptotic approximation of target states
* (Optional) PPT criterion and basic structure of PPT-entangled states

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-81 (Quantum theory)
* ams-94 (Information and communication theory)
* ams-47 (Operator theory)
* ams-15 (Linear and multilinear algebra; matrix theory)

### Choose either option

* [ ] I plan on adding this conjecture to the repository
* [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---

No repository file, test, or entry point is named. Start by reviewing existing formalized conjectures in formal-conjectures and the cited quantum-information references, then determine how the definitions and main equivalence can be represented in Lean. Done means the conjecture and its supporting definitions are formally added to the repository.

Written by the indexing model from the issue text.