Pith. sign in

REVIEW 2 major objections 6 minor 40 references

A Lean library formally proves the data-processing inequality for sandwiched Rényi relative entropy on finite-dimensional quantum systems.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-11 06:54 UTC pith:TRFLMKPD

load-bearing objection A real Lean library that machine-checks the finite-dimensional sandwiched Rényi DPI and fills a known gap for the generalized quantum Stein’s lemma formalization. the 2 major comments →

arxiv 2607.05492 v1 pith:TRFLMKPD submitted 2026-07-06 quant-ph cs.AI

Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information

Kazumi Kasaura , Kei Tsukamoto , Kento Mori , Risa Mizuno , Takahiro Namatame , Yuta Oriike , Masaya Taniguchi , Sho Sonoda
show 1 more author
Hayata Yamasaki
This is my paper
classification quant-ph cs.AI MSC 81P4568V2046L6047A63 PACS 03.67.-a03.65.Fd
keywords sandwiched Rényi relative entropydata-processing inequalityLean 4formal verificationquantum channelsLieb–Ando inequalitiesstrong subadditivitygeneralized quantum Stein's lemma
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper builds a reusable Lean 4 library for finite-dimensional quantum information and uses it to machine-check the data-processing inequality for the sandwiched Rényi relative entropy. That inequality says a standard quantum divergence cannot increase when both arguments are sent through the same completely positive trace-preserving channel. The library supplies a basis-independent operator interface compatible with Mathlib, a hierarchy of noncommutative trace inequalities, and entropy-specific ingredients such as Young-based variational formulas and Haar averaging. As immediate payoffs it recovers strong subadditivity-type inequalities and supplies the missing formal piece needed to finish a Lean proof of the generalized quantum Stein’s lemma. The larger aim is machine-checkable foundations that humans and AI systems can reuse for further quantum-information theorems.

Core claim

The authors construct a Lean 4 library that fully formalizes the data-processing inequality for the sandwiched Rényi relative entropy for positive-semidefinite operators on finite-dimensional quantum systems, first on the positive-definite cone and then by an extended-real extension to the positive-semidefinite case, and show that the same development yields strong subadditivity as a corollary and closes the remaining gap in an existing formalization of the generalized quantum Stein’s lemma.

What carries the argument

The data-processing inequality for the sandwiched Rényi relative entropy (and its quasi-entropy Q_α), proved by combining Young/reverse-Young variational formulas, Lieb–Ando trace inequalities obtained via generalized perspectives and operator power means on Hilbert–Schmidt spaces, Stinespring dilation, and normalized Haar averaging.

Load-bearing premise

Everything is proved only for finite-dimensional quantum systems; invertibility, spectra, unitary Haar measure, and continuous functional calculus are all handled in that setting, so the formal claim does not yet cover infinite-dimensional systems.

What would settle it

Inspect the public Lean repository: if the kernel accepts the stated DPI theorems for sandwiched Rényi relative entropy (positive-definite core and positive-semidefinite extension) without sorry placeholders, and the same library discharges the corresponding gap in the generalized quantum Stein’s lemma development, the central claim holds; any remaining sorry or type mismatch falsifies it.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The manuscript presents Lean-Quantum, a Lean 4 library for finite-dimensional quantum information theory, and uses it to formalize the data-processing inequality (DPI) for the sandwiched Rényi relative entropy of positive semidefinite operators. The library supplies a basis-independent, Mathlib-compatible interface for systems, states, CPTP maps, tensor products, partial traces, Choi/Kraus/Stinespring representations, and a hierarchy of noncommutative trace inequalities (Löwner–Heinz, block positivity, Hilbert–Schmidt spaces, Jensen, generalized perspectives, operator power means, Lieb–Ando). Entropy-specific ingredients include Young/reverse-Young variational formulas for the sandwiched quasi-entropy, tensor-product CFC identities, and Haar averaging. The DPI is proved first on the positive-definite cone (Theorem 1) and extended to the PSD setting via an extended-real non-negative divergence; strong subadditivity is obtained as a corollary, and the formalization is positioned as the missing DPI ingredient for completing prior Lean work on the generalized quantum Stein’s lemma.

Significance. If the formalization is as claimed, this is a substantial contribution to machine-checked quantum information theory: a reusable, coordinate-free operator interface aligned with Mathlib; a modular hierarchy of trace inequalities that is not DPI-specific; and a fully formalized cornerstone inequality (sandwiched Rényi DPI) with SSA as a corollary. The alternative variational route via trace Young and reverse-Young inequalities (instead of Euler–Lagrange optimization on the positive cone) is a genuine formalization-friendly reorganization of the Frank–Lieb strategy and is of independent interest. Public code and explicit intermediate interfaces are real strengths for AI-assisted and human formal work. The finite-dimensional scope is clearly stated and appropriate for the claimed applications.

major comments (2)
  1. §I.E and Abstract: the claim that the library supplies “the last missing component needed to complete the Lean formalization of the generalized quantum Stein’s lemma” is load-bearing for the stated applications but is supported only by citation to prior work with sorry and a private communication [40]. The manuscript does not exhibit a completed, sorry-free Stein formalization that imports the new DPI. Either demonstrate the integration (or a public bridge) or soften the wording to “supplies the analytic DPI component required by existing developments.”
  2. §IV.D: Theorem 1 is stated carefully for the positive-definite cone, but the final PSD/extended-real DPI—which is the central formalization claim of the abstract—is described mainly in prose (regularization σ↦σ+εI, support conventions) without a theorem statement of comparable precision (hypotheses on supports, extended-real conventions, and the exact monotone quantity). For a machine-checked cornerstone result, the manuscript should state the PSD theorem as explicitly as Theorem 1, including the precise Lean-level predicates used.
minor comments (6)
  1. §I.C / throughout: “Löewner–Heinz” appears with an extra “e”; standardize to “Löwner–Heinz” (as in §III.A and the references).
  2. §II.B: the long instance blocks transporting C*-algebra and StarOrderedRing structure from continuous linear maps are useful for implementers but dense for readers; a short mathematical summary of what is transported would help.
  3. §IV.A: the reverse-Young scalar core (Eq. near (54)) and the equality-case optimizer for 0<α<1 are central to the claimed alternative proof; a short explicit construction of the optimizer (as for α>1) would make the human-readable contribution clearer without requiring the Lean sources.
  4. §IV.C: the Stinespring–Haar identity (Eq. (63)–(64)) mixes environment and system factors; a one-line diagram of tensor-factor conventions relative to Tr2 / TrRight would reduce ambiguity.
  5. References: several 2025–2026 arXiv items and the private communication [40] are hard to verify; ensure stable links or DOIs where available, and prefer public artifacts over private communication for the Stein-completion claim.
  6. Abstract and §V: “AI-assisted formalization” is a framing theme; a brief concrete note on what was AI-assisted versus human-designed (as hinted in §I.C) would set expectations without overselling automation.

Circularity Check

0 steps flagged

No significant circularity: the paper formalizes a known analytic theorem via modular Lean lemmas rather than deriving a prediction from its own inputs.

full rationale

The central claim is a machine-checked Lean 4 formalization of the data-processing inequality for the sandwiched Rényi relative entropy on finite-dimensional systems (Theorem 1 on the positive-definite cone, then the extended-real PSD extension), together with reusable operator-theoretic infrastructure. The mathematical endpoint is the classical Frank–Lieb DPI; the paper reorganizes the proof (Young/reverse-Young variational formulas for Q_α, generalized perspectives → operator power means → Lieb–Ando, Stinespring + Haar averaging + Jensen, tensor CFC multiplicativity, log monotonicity) into Mathlib-compatible intermediate statements. None of the load-bearing steps define the DPI in terms of itself, fit a free parameter to data and re-label it a prediction, or import an unverified uniqueness theorem from the same authors to force the result. Self-references to the public library [1] and to prior Stein-lemma formalization work [13, 34] that left the DPI as sorry are infrastructure citations; the DPI itself is proved from the library’s own lemmas rather than assumed. Finite-dimensional restriction (Qudit) is stated explicitly and does not create a definitional loop. Score 0 is therefore the correct, proportionate finding.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 0 invented entities

No empirical free parameters. The claim rests on standard finite-dimensional quantum mechanics and Mathlib-backed analysis (CFC, Haar measure, Bochner integrals, C*-order), plus the domain restriction to finite-dimensional systems and the authors’ chosen proof architecture (PD cone first; Young-based variational formulas; perspectives → power means → Lieb–Ando). No new physical entities are postulated.

axioms (5)
  • domain assumption Finite-dimensional complex Hilbert spaces (Qudit) as the ambient setting for systems, channels, spectra, and Haar unitary averages.
    Stated throughout §II and used for all DPI theorems; infinite-dimensional extensions are out of scope.
  • standard math Mathlib continuous functional calculus, ordered C*-algebra structure, spectra, and related operator-algebra facts for real powers and positivity.
    Core of §§II–III; the library transports linear endomorphisms to continuous linear maps / C*-structure rather than reproving analysis from scratch.
  • standard math Existence/normalization of Haar measure on compact unitary groups and Bochner-integral Jensen inequalities in finite dimension.
    §IVC uses these to convert partial traces into unitary averages in the Stinespring step of the DPI.
  • standard math Standard finite-dimensional equivalences among complete positivity, Choi positivity, Kraus, and Stinespring representations.
    Formalized in §IIB and used to replace channels by dilations in the DPI proof.
  • ad hoc to paper Proof architecture choice: establish DPI first on positive-definite operators, then extend via extended-real non-negative divergence and regularization.
    Explicit design choice in §§I.C and IV; not a new physical law, but load-bearing for how invertibility and support conditions are handled in Lean.

pith-pipeline@v1.1.0-grok45 · 35858 in / 2874 out tokens · 21766 ms · 2026-07-11T06:54:08.139720+00:00 · methodology

0 comments
read the original abstract

Quantum information theory is built on entropic quantities; among them, the sandwiched R\'enyi relative entropy is a fundamental divergence with various applications, and its data processing inequality (DPI) under quantum channels is a cornerstone result. In this work, we present a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis. As a central demonstration of the library, we formalize the DPI for the sandwiched R\'enyi relative entropy for positive semidefinite operators on finite-dimensional quantum systems. The library provides a basis-independent operator-theoretic framework for finite-dimensional quantum mechanics compatible with the standard mathematical library Mathlib, including reusable interfaces for finite-dimensional systems, states, channels, tensor products, partial traces, Choi operators, Kraus representations, and Stinespring representations. It also builds infrastructure for noncommutative trace inequalities, including operator monotonicity and convexity via the real continuous functional calculus, block-operator positivity, Hilbert-Schmidt operator spaces, Jensen's operator inequality, generalized perspectives, operator power means, and Lieb-Ando trace inequalities. On top of this framework, we formalize entropy-specific ingredients for the DPI: variational formulas for the sandwiched quasi-entropy via Young and reverse-Young inequalities, tensor-product compatibility of real powers, and Haar measures on unitary groups. Together, these components yield a Lean formalization of the DPI, give strong subadditivity as a corollary, and provide the last missing component needed to complete the Lean formalization of the generalized quantum Stein's lemma. More broadly, the development provides machine-checkable foundations for future formalized and AI-assisted research in quantum information theory.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

40 extracted references · 6 linked inside Pith

  1. [1]

    Kasaura, K

    K. Kasaura, K. Tsukamoto, K. Mori, R. Mizuno, T. Namatame, Y. Oriike, M. Taniguchi, S. Sonoda, and H. Yamasaki, Lean quantum,https://github.com/Hayata-Yamasaki-Group/lean-quantum(2026)

    2026

  2. [2]

    Watrous,The Theory of Quantum Information(Cambridge University Press, 2018)

    J. Watrous,The Theory of Quantum Information(Cambridge University Press, 2018)

    2018

  3. [3]

    Müller-Lennert, F

    M. Müller-Lennert, F. Dupuis, O. Szehr, S. Fehr, and M. Tomamichel, On quantum rényi entropies: A new generalization and some properties, Journal of Mathematical Physics54(2013)

    2013

  4. [4]

    M. M. Wilde, A. Winter, and D. Yang, Strong converse for the classical capacity of entanglement-breaking and hadamard channels via a sandwiched rényi relative entropy, Communications in Mathematical Physics331, 593 (2014)

    2014

  5. [5]

    Jakšić, Y

    V. Jakšić, Y. Ogata, Y. Pautrat, and C.-A. Pillet, Entropic fluctuations in quantum statistical mechanics. an introduction. quantum theory from small to large scales, Lecture Notes of the Les Houches Summer School95, 978

  6. [6]

    R. L. Frank and E. H. Lieb, Monotonicity of a relative rényi entropy, Journal of Mathematical Physics54(2013)

    2013

  7. [7]

    Beigi, Sandwiched rényi divergence satisfies data processing inequality, Journal of Mathematical Physics54(2013)

    S. Beigi, Sandwiched rényi divergence satisfies data processing inequality, Journal of Mathematical Physics54(2013)

    2013

  8. [8]

    Javadi-Abhari, M

    A. Javadi-Abhari, M. Treinish, K. Krsulich, C. J. Wood, J. Lishman, J. Gacon, S. Martiel, P. D. Nation, L. S. Bishop, A. W. Cross, B. R. Johnson, and J. M. Gambetta, Quantum computing with qiskit (2024), arXiv:2405.08810 [quant-ph]

    Pith/arXiv arXiv 2024

  9. [9]

    Suzuki, Y

    Y. Suzuki, Y. Kawase, Y. Masumura, Y. Hiraga, M. Nakadai, J. Chen, K. M. Nakanishi, K. Mitarai, R. Imai, S. Tamiya, T. Yamamoto, T. Yan, T. Kawakubo, Y. O. Nakagawa, Y. Ibe, Y. Zhang, H. Yamashita, H. Yoshimura, A. Hayashi, and K. Fujii, Qulacs: a fast and versatile quantum circuit simulator for research purpose, Quantum5, 559 (2021)

    2021

  10. [10]

    Gidney, Stim: a fast stabilizer circuit simulator, Quantum5, 497 (2021)

    C. Gidney, Stim: a fast stabilizer circuit simulator, Quantum5, 497 (2021)

    2021

  11. [11]

    L. d. Moura and S. Ullrich, The lean 4 theorem prover and programming language, inInternational Conference on Auto- mated Deduction(Springer, 2021) pp. 625–635

    2021

  12. [12]

    The mathlib Community, The Lean Mathematical Library, inProceedings of the 9th ACM SIGPLAN International Con- ference on Certified Programs and Proofs, CPP 2020 (ACM, New Orleans, LA, USA, 2020)

    2020

  13. [13]

    Meiburg, L

    A. Meiburg, L. A. Lessa, and R. R. Soldati, A formalization of the generalized quantum stein’s lemma in lean (2025), arXiv:2510.08672 [quant-ph]

    arXiv 2025

  14. [14]

    X. He, S. Lu, and B. Zeng, Co-designing quantum codes with transversal diagonal gates via multi-agent systems (2026), arXiv:2510.20728 [quant-ph]

    Pith/arXiv arXiv 2026

  15. [15]

    Y. Ren, J. Li, and Y. Qi, Merlean: An agentic framework for autoformalization in quantum computation (2026), arXiv:2602.16554 [cs.LO]

    arXiv 2026

  16. [16]

    Ehatamm, Y

    M. Ehatamm, Y. Lee, X. Wu, and R. Tao, End-to-end formalization of quantum error correction (2026), arXiv:2605.16523 [quant-ph]

    Pith/arXiv arXiv 2026

  17. [17]

    U. Kol, M. Ben-Shahar, K. Sulimany, and D. Englund, A machine-verified proof of a quantum-optimization conjecture (2026), arXiv:2606.29687 [quant-ph]

    Pith/arXiv arXiv 2026

  18. [18]

    Hansen and G

    F. Hansen and G. Kjærgård Pedersen, Jensen’s inequality for operators and löwner’s theorem, Mathematische Annalen 258, 229 (1982)

    1982

  19. [19]

    E. G. Effros, A matrix convexity approach to some celebrated quantum inequalities, Proceedings of the National Academy of Sciences106, 1006 (2009)

    2009

  20. [20]

    Ebadian, I

    A. Ebadian, I. Nikoufar, and M. Eshaghi Gordji, Perspectives of matrix convex functions, Proceedings of the National Academy of Sciences108, 7313 (2011). 34

    2011

  21. [21]

    Kubo and T

    F. Kubo and T. Ando, Means of positive linear operators, Mathematische Annalen246, 205 (1980)

    1980

  22. [22]

    E. A. Carlen, Trace inequalities and quantum entropy: an introductory course, Entropy and the Quantum529, 73 (2010)

    2010

  23. [23]

    Nikoufar, A

    I. Nikoufar, A. Ebadian, and M. Eshaghi Gordji, The simplest proof of lieb concavity theorem, Advances in Mathematics 248, 531 (2013)

    2013

  24. [24]

    Löwner, Über monotone matrixfunktionen, Mathematische Zeitschrift38, 177 (1934)

    K. Löwner, Über monotone matrixfunktionen, Mathematische Zeitschrift38, 177 (1934)

    1934

  25. [25]

    Heinz, Beiträge zur störungstheorie der spektralzerleung, Mathematische Annalen123, 415 (1951)

    E. Heinz, Beiträge zur störungstheorie der spektralzerleung, Mathematische Annalen123, 415 (1951)

    1951

  26. [26]

    F. G. S. L. Brandão and M. B. Plenio, Entanglement theory and the second law of thermodynamics, Nature Physics4, 873–877 (2008)

    2008

  27. [27]

    F. G. Brandao and M. B. Plenio, A reversible theory of entanglement and its relation to the second law, Communications in Mathematical Physics295, 829 (2010)

    2010

  28. [28]

    F. G. Brandao and M. B. Plenio, A generalization of quantum Stein’s lemma, Communications in Mathematical Physics 295, 791 (2010)

    2010

  29. [29]

    F. G. S. L. Brandão and G. Gour, Reversible framework for quantum resource theories, Phys. Rev. Lett.115, 070503 (2015)

    2015

  30. [30]

    Hayashi and H

    M. Hayashi and H. Yamasaki, The generalized quantum Stein’s lemma and the second law of quantum resource theories, Nature Physics21, 1988 (2025)

    1988

  31. [31]

    Lami, A Solution of the Generalized Quantum Stein’s Lemma, IEEE Transactions on Information Theory71, 4454 (2025)

    L. Lami, A Solution of the Generalized Quantum Stein’s Lemma, IEEE Transactions on Information Theory71, 4454 (2025)

    2025

  32. [32]

    K. Fang, G. Gour, and X. Wang, Towards the ultimate limits of quantum channel discrimination and quantum communi- cation, Science China Information Sciences68, 180509 (2025)

    2025

  33. [33]

    Berta, F

    M. Berta, F. G. S. L. Brandão, G. Gour, L. Lami, M. B. Plenio, B. Regula, and M. Tomamichel, On a gap in the proof of the generalised quantum Stein’s lemma and its consequences for the reversibility of quantum resources, Quantum7, 1103 (2023)

    2023

  34. [34]

    Meiburg and contributors, Lean quantum information,https://github.com/Timeroot/Lean-QuantumInfo

    A. Meiburg and contributors, Lean quantum information,https://github.com/Timeroot/Lean-QuantumInfo

  35. [35]

    Physlib, Physlib: The lean physics,https://reservoir.lean-lang.org/@leanprover-community/Physlib

  36. [36]

    Hietala, R

    K. Hietala, R. Rand, S.-H. Hung, X. Wu, and M. Hicks, A verified optimizer for quantum circuits, Proceedings of the ACM on Programming Languages5, 1–29 (2021)

    2021

  37. [37]

    Bordg, H

    A. Bordg, H. Lachnitt, and Y. He, Certified quantum computation in isabelle/hol, Journal of Automated Reasoning65, 691–709 (2020)

    2020

  38. [38]

    Y. Peng, K. Hietala, R. Tao, L. Li, R. Rand, M. Hicks, and X. Wu, A formally certified end-to-end implementation of shor’s factorization algorithm (2022), arXiv:2204.07112 [cs.PL]

    Pith/arXiv arXiv 2022

  39. [39]

    L. Zhou, G. Barthe, P.-Y. Strub, J. Liu, and M. Ying, Coqq: Foundational verification of quantum programs (2022), arXiv:2207.11350 [cs.PL]

    Pith/arXiv arXiv 2022

  40. [40]

    Meiburg, Private communication (2026)

    A. Meiburg, Private communication (2026)

    2026