Seeking formal verification directions in quantum informatio

Stream: PhysLean

[Ruize Chen]

Hi everyone,

I’m a mathematics student at Imperial College London, currently studying quantum information and quantum computing, with a solid background in quantum mechanics.

On the Lean side, I’ve worked on algebraic topology proofs (e.g. fundamental group of S¹ and path-based reasoning), so I’m familiar with the mathlib ecosystem.

Recently I’ve been exploring how formal verification could be applied to quantum information, and I’ve started reading through the existing code in the Lean-QuantumInfo project. From what I can tell, the most natural foundation—both mathematically and physically—seems to lie around QuantumInfo/Finite/Qubit/Basic.lean.

I’d like to confirm whether this is indeed a good place to start building formal verification structures, and hear thoughts on what kinds of definitions or theorems in quantum information might be meaningful to formalize next (for example, tensor product structures, quantum channels, or simple measurement postulates).

Any advice or perspective on connecting formal verification ideas to quantum information theory would be greatly appreciated.

[ZhiKai Pong]

Quantuminfo has a dedicated channel here:
#Quantum information
so you can ask over there if you have more specific ideas.

this conversation a while ago might be of interest:
#PhysLean > Quantum computing

where it was mentioned that some concepts might be useful in PhysLean as well, but I believe PhysLean has virtually nothing on this right now so depends on what direction you'd like to take :)