Formalize Open Quantum Problem #7: Additivity of Entanglement of Formation

### What is the conjecture

This is problem [#7](https://oqp.iqoqi.oeaw.ac.at/additivity-of-entanglement-of-formation) in [Krüger & Werner’s snapshot](https://arxiv.org/abs/quant-ph/0504166) of Reinhard F. Werner’s open-problems collection, later [maintained by a community of quantum researchers](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (resolution: **negative answer**, via Hastings’ counterexample to the “additivity conjectures” for quantum channels, together with Shor’s equivalence results).

> **Problem (Open Quantum Problem #7: “Additivity of Entanglement of Formation”).**
> The entanglement of formation is subadditive under tensor products. Show that it is always **additive**, or else give a counterexample.

Concretely:

* Let `ρ` be a bipartite **density operator** on `H_A ⊗ H_B`. The **entanglement of formation** `E_F(ρ)` is defined by the convex-roof / variational formula
`E_F(ρ) = inf { ∑_i r_i S( (ρ_i)|_A ) | ρ = ∑_i r_i ρ_i }`,
where `r_i ≥ 0`, `∑_i r_i = 1`, each `ρ_i` is a density operator, `S(σ) = -Tr(σ log σ)` is the von Neumann entropy, and `(ρ_i)|_A = Tr_B(ρ_i)` is the restriction to Alice’s subsystem.
Since `S` is concave, the infimum is attained on ensembles of **pure states** (so one often restricts to decompositions `ρ = ∑_i r_i |ψ_i⟩⟨ψ_i|`).

* Given two bipartite states `ρ^(1)` on `H_{A1} ⊗ H_{B1}` and `ρ^(2)` on `H_{A2} ⊗ H_{B2}`, form
`ρ = ρ^(1) ⊗ ρ^(2)`,
and regard it as bipartite with parties `(A1A2)` and `(B1B2)`.

Then one always has the easy inequality
`E_F(ρ^(1) ⊗ ρ^(2)) ≤ E_F(ρ^(1)) + E_F(ρ^(2))`
(by taking the tensor product of optimal (or approximately optimal) ensembles and using entropy additivity on product states).

The conjecture / open question was:

* **Additivity conjecture:** for all bipartite states `ρ^(1), ρ^(2)`,
`E_F(ρ^(1) ⊗ ρ^(2)) = E_F(ρ^(1)) + E_F(ρ^(2))`.

This additivity question is tightly connected to (and, in a strong sense, equivalent to) a family of additivity questions for quantum channels (Holevo capacity / minimum output entropy), as explained by Shor; the OQP page explicitly notes equivalence to [Problem #10](https://oqp.iqoqi.oeaw.ac.at/additivity-of-classical-capacity-and-related-problems).

**Solved / resolution (negative answer):** Hastings constructed counterexamples to the global additivity conjectures for quantum channels (in particular, violations of additivity of the minimum output entropy / Holevo quantity). By Shor’s equivalence theorem, this implies that **entanglement of formation is not additive in general**, i.e. there exist bipartite states `ρ^(1), ρ^(2)` such that
`E_F(ρ^(1) ⊗ ρ^(2)) < E_F(ρ^(1)) + E_F(ρ^(2))`.

(So a good formalization target is to record the original conjecture and then formalize a theorem/counterexample showing it is false, e.g. via the Shor equivalence + Hastings counterexample route.)

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #7)](https://oqp.iqoqi.oeaw.ac.at/additivity-of-entanglement-of-formation)
* [Solved Quantum Problems list (marks #7 solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
* O. Krüger & R. F. Werner, “Some Open Problems in Quantum Information Theory” (see “Problem 7”):

* [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 references on the problem page:

* C. H. Bennett, D. P. DiVincenzo, J. A. Smolin, W. K. Wootters, “Mixed-state entanglement and quantum error correction” (Phys. Rev. A 54, 3824 (1996)), arXiv: [quant-ph/9604024](https://arxiv.org/abs/quant-ph/9604024)
* G. Vidal, W. Dür, J. I. Cirac, “Entanglement cost of mixed states” (Phys. Rev. Lett. 89, 027901 (2002)), arXiv: [quant-ph/0112131](https://arxiv.org/abs/quant-ph/0112131)

Equivalence to other additivity conjectures:

* P. W. Shor, “Equivalence of additivity questions in quantum information theory” (quant-ph/0305035; published Commun. Math. Phys. 246, 453 (2004)):

* [https://arxiv.org/abs/quant-ph/0305035](https://arxiv.org/abs/quant-ph/0305035)

Resolution / negative answer (via counterexample to additivity conjectures):

* M. B. Hastings, “Superadditivity of communication capacity using entangled inputs” (arXiv: [0809.3972](https://arxiv.org/abs/0809.3972); published Nature Physics 5, 255–257 (2009))

(Optionally helpful: follow-up expositions simplifying/clarifying the Hastings construction exist, e.g. Brandão–Horodecki 2009.)

### Prerequisites needed

* Finite-dimensional quantum mechanics: density matrices, tensor products, partial trace
* Von Neumann entropy and its basic properties (concavity; additivity on product states)
* Convex analysis / convex roofs: understanding “inf over decompositions” and why the optimum can be taken over pure-state ensembles
* Basic entanglement theory: entanglement measures / monotones; operational motivation via entanglement cost (optional but motivating)
* (For the “solved” direction via equivalences) quantum channels (CPTP maps), Holevo quantity / classical capacity notions, and Shor’s equivalence between additivity conjectures (plus Hastings’ counterexample framework)

### [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)

### 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

---

The payload names no repository files, tests, or Lean entry points, so begin by surveying existing formalizations in the formal-conjectures repository and checking how density operators, entropy, tensor products, and quantum channels are represented. Decide whether the scope is the original additivity statement or the negative resolution, then use Shor’s equivalence and Hastings’ counterexample references to define what a completed formalization must establish.

Written by the indexing model from the issue text.