vqc_in_lean is a Lean 4 port of the Verified Quantum Computing (VQC) project, originally implemented using the Coq proof assistant. This project aims to provide a formal foundation for quantum computing and the verification of quantum programs using Lean 4 and mathlib4.
Note: This project is created as part of my personal learning journey in Lean 4 and quantum computing. It is not intended for production use or as an officially supported educational resource. Feedback and suggestions are welcome as I refine my understanding of these topics.
Inspired by Ben Caldwell and Robert Rand’s Verified Quantum Computing tutorial.