QFormal is an effort led by Alex Meiburg, Leonardo Lessa, and Rodolfo Soldati at the University of Waterloo and the Perimeter Institute for Theoretical Physics.
We focus on formalizing quantum information theory in Lean 4. PLACEHOLDER for more details about our mission, goals, and current projects.