Entanglement without secret key and the PPT-squared conjecture
From OpenAI Aftermath
Entanglement without secret key and the PPT-squared conjecture concerns two questions in quantum information theory. The first, posed as Problem 24 in Krüger and Werner's open-problem collection with P. Horodecki as contact, asks whether every entangled state allows two parties to distil a secret key. The second, the PPT-squared conjecture of Christandl, asks whether the composition of two quantum maps that are positive under partial transposition (PPT) is always entanglement breaking. A manuscript dated 27 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims an entangled state in dimension 10 × 10 with zero distillable secret key, and explicit PPT maps whose composition is not entanglement breaking, including a trace-preserving PPT channel whose square is not entanglement breaking. The collection includes Lean formalizations of the composition statements. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- PPT entangled states have zero distillable entanglement (Horodecki, Horodecki and Horodecki), yet some PPT entangled states have positive distillable secret key; the private-state description explains how secrecy can persist without singlet distillation. Separable states have zero key against a purifying eavesdropper. The converse, whether every entangled state has positive key, is Problem 24 of Krüger and Werner's collection (2005).
- Quantitative obstructions near private bits were given by Kim and Sanders and by Badziąg and coauthors, with bounds depending on the shield dimension. Pauwels, Gisin and Renner recently constructed a classical bipartite source with positive secrecy formation cost and zero asymptotic key rate, and proved positive two-way key for some bound-entangled two-qutrit states.
- The PPT-composition conjecture in the form used is Conjecture IV.1 of Christandl, Müller-Hermes and Wolf (2019); the channel version is Problem G of the 2012 BIRS workshop report.
The original results
- Claims. Theorem 1.1 of Entanglement with zero distillable secret key in local dimension ten states that there is an explicitly specified entangled density operator on C10 ⊗ C10, whose range contains no nonzero product vector, with zero distillable secret key: for every protocol in the paper's admitted class (local instruments with authenticated two-way public communication, completed almost surely, against an eavesdropper holding a purification and the public record), the output stays at trace-norm distance at least 1/5, so at trace distance at least 1/10, from every ideal key bit. Theorem 1.2 gives two explicit PPT maps on 10 × 10 matrices whose composition is not entanglement breaking, refuting the two-map composition conjecture; Theorem 1.3 gives a trace-preserving PPT channel on 21 × 21 matrices whose square is not entanglement breaking. The manuscript does not claim that either dimension is minimal.
- Method, as described: states of the form (L ⊗ M)(χχ*) with PPT maps L, M form a class stable under tensor powers. For this class a coherence inequality bounds the overlap of Eve's conditional states on the 00 and 11 branches by the probability that the two bits differ, which gives the uniform gap for any number of copies. The Choi matrix of a composition of two PPT maps lies in the class. Entanglement is shown by the range criterion: a PPT map on 4 × 4 matrices is singular at twenty projective directions, no nonzero quadratic in four variables vanishes at ten of them, and a product vector in the range would give two quadratics covering all twenty directions, although each covers at most nine.
- Sources. The manuscript Entanglement with zero distillable secret key in local dimension ten at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization covers the two PPT-composition consequences: the explicit pair on 10 × 10 matrices whose composition is not entanglement breaking and has no nonzero product vector in the range of its Choi matrix, and the trace-preserving PPT channel on 21 × 21 matrices whose square is not entanglement breaking. The zero-distillable-key statement is outside the formalization. The Comparator statements are
DimensionTenPair.leanandDimensionTenChannel.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 21 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial" and records Comparator passes for both challenges. Its note states that the primary claim, the entangled state with zero distillable secret key, is not stated in Lean, and that the formalized statements are the PPT-squared counterexample and the explicit pair. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-09 | Pico (Håkon Åmdal), row 272 in piiiico/openai-math-counterexamples (GitHub; commit b82e9d7) |
Verification (explicit certificate) | Checks the explicit integer matrices behind the state: the commutation identities that make the basic map PPT, and the claim that the rank-deficient directions are exactly twenty points, by enumerating these complex points directly, a route the manuscript's own checker does not take. Reports "holds". | Part of a census of counterexample families in the collection. It does not check the secret-key argument. |
| 2026-10-10 | cert-machine, openai/math lane K: runs 38019899278 (DimensionTenChannel) and 38051470892 (DimensionTenPair) |
Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept both solutions, in 2,229 s and 1,714 s; an earlier run of DimensionTenChannel did not complete. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists neither challenge, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and one minor note: the admitted-protocol model for countable or measurable schedules is nonstandard and heavy, so the zero-key statement for infinite protocols holds within the model as defined; for ordinary finite-round protocols the reviewer calls the setup standard and correct. The reviewer read most sections in full but not the independent second construction in the projection and combinatorial sections. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
