The quantum formalism:

Sheldon Goldstein, Roderich Tumulka, Nino Zanghı̀

Philip Goyal

In this paper and a companion paper, we attempt to systematically investigate the possibility that the concept of information may enable a derivation of the quantum formalism from a set of physically comprehensible postulates. To do so, we formulate an abstract experimental set-up and a set of assumptions based on generalizations of experimental facts that can be reasonably taken to be representative of quantum phenomena, and on theoretical ideas and principles, and show that it is possible to deduce the quantum formalism. In particular, we show that it is possible to derive the abstract quantum formalism for finite-dimensional quantum systems and the formal relations, such as the canonical commutation relationships and Dirac's Poisson Bracket rule, that are needed to apply the abstract formalism to particular systems of interest. The concept of information, via an information-theoretic invariance principle, plays a key role in the derivation, and gives rise to some of the central structural features of the quantum formalism.

R. Guy Woolley

Olivier Brunet

In this work, we present a logical formalism for reasoning about quantum systems in finite dimension. Contrary to the usual approach in quantum logic, our formalism is based classical first-order logic, which allows us to use the tools of model theory in our study. In particular, we show that our formal theory is complete, meaning that it entirely determines the behaviour of quantum systems. Moreover, we provide a characterization of the models of our formal theory, thus providing new insights in the study of hidden variable models of quantum theory.

Nimrod Moiseyev

This book is dedicated to the non-Hermitian formalism of quantum mechanics. In this chapter we wish to give the motivation and the rational for developing a non-Hermitian formalism to quantum mechanics. Therefore this chapter will not explain how non-Hermitian calculations are carried out or in what way the non-Hermitian formalism is analogous to the standard (Hermitian) formalism of quantum mechanics. It is important to emphasize that there is no (known) transformation which enables one to map results which were obtained using one formalism to the other one. Yet, the same physical results should be obtained by studying the same phenomenon using the two formalisms. If this is the case, why should one bother to develop an alternative formalism to the standard Hermitian formalism of quantum mechanics? There are several reasons for doing this and here we shall focus on five of those reasons. (1) There are phenomena which can be explained in a straightforward fashion using the non-Hermitian formalism but are very hard and often impossible to explain within the framework of the standard (Hermitian) formalism of quantum mechanics . In particular in Chapter 9 we will describe several physical phenomena which are associated with the self-orthogonality where two or more degenerate resonance states are coalesced. (2) There are physical phenomena which one might not immediately associate with quantum behavior where the quantum language can be used to describe the physics . The studied problem may be, for example, in systems described in terms of classical statistical mechanics, diffusion in biological systems, or propagation of light in waveguides (WG). […]

Lei Zhang, Yusheng Zhao, Hongshun Yao +1 more

Large language models are increasingly assisting with demanding formal theorem-proving tasks, particularly when grounded in machine-checked libraries such as Lean. Agentic systems further amplify this process by searching, reusing, and extending existing formal developments to uncover new discoveries. In quantum computing, Shor's algorithm and its variants present such a demanding case for Lean formalization. In this work, we formalize this algorithm family in Lean through agentic formalization: software agents analyze sources, write Lean code and repair proofs, with human review of the scientific claims and machine checking of the resulting formal proofs. Our formalization develops the mathematical foundations for analyzing quantum attacks in two cryptographic settings: a 2048-bit modulus in the RSA-2048 and the standardized elliptic curve over a 256-bit prime field (P-256). To support these analyses, the formalization ranges from quantum algorithms for order finding to reversible quantum circuits for modular and elliptic-curve arithmetic. Based on [Quantum 5, 433] and [ASIACRYPT 2017, 241--270], we formalize the logical resource estimates for RSA-2048 and P-256, respectively, and provide additional estimates of classical operations. We expect the results pave the way for broader machine-checked quantum cryptanalysis and represent a step toward AI-assisted design and verification of quantum algorithms.