Automated Reasoning for Quantum Mechanics

WE Heraeus - Lorentz Workshop

13 Jul - 17 Jul 2026

Where:

Lorentz Center, Leiden

Scientific organizers:

Alfons Laarman, U Leiden, The Netherlands • Kuldeep Meel, Georgia Institute of Technology, USA • Robert Wille, TU Munich • 
Natalia Chepiga, TU Delft, The Netherlands

Progress in materials science, quantum computing, and networking depends greatly on our ability to simulate and analyze quantum mechanical systems. For this purpose, the physics community has developed powerful formalisms such as tensor networks, quantum neural networks, and the stabilizer tableau. Their tailored application to specific quantum mechanical systems, such as Ising and Potts models, led to many breakthroughs. However, these methods all have limitations when dealing with the unavoidable combinatorial nature of simulating quantum mechanics. They also behave differently, with orthogonal strengths in many cases. For instance, the stabilizer formalism can handle certain systems with high entanglement, but tensor networks, such as matrix product states, cannot.

To boost our ability to simulate quantum mechanical systems, we believe that insights from theoretical computer science perfectly complement the existing knowledge in physics. In particular, our own recent research has shown that automated reasoning techniques, originally developed to analyze complex (classical) information systems, show great promise in the domain of quantum mechanics. Moreover, these new approaches have been shown to break boundaries between existing approaches, combining their strengths and overcoming individual limitations. Based on these developments, we aim to realize fundamentally novel formalisms for representing and processing quantum information.

The proposed workshop brings physics and computer science experts together to realize the above vision. We believe that the combination of their respective insights will lead to formalisms necessary to analyze larger and more complex quantum mechanical systems, while obviating the need for tailor-made solutions in many cases.