Maintainers
The following individuals are the maintainers of this project. They have the power to approve the merger of pull requests, and the responsibility to ensure that the project is well-maintained and that the codebase is of high quality.
If you would like to contact the maintainers, please use the Lean Zulip.
Léo Lessa
Leonardo (Léo) is a PhD student at the Perimeter Institute and University of Waterloo working on
quantum information theory disguised as condensed matter.
He has been involved in formalizing physics since 2024.
Alex Meiburg
Alex is a postdoctoral fellow at the Perimeter Institute and University of Waterloo's IQC.
He has a PhD in condensed matter theory at the University of California, Santa Barbara.
He's been contributing to Mathlib since 2023.
Daniel Morrison
Daniel is a Lean contractor for Harmonic. They have a PhD in symplectic geometry
from the University of California, Irvine and has been working with Lean formalization since 2023.
Zhi Kai Pong
Zhi Kai is an optical engineer with a PhD in femtosecond laser direct writing from the University of Oxford.
He has been involved in the formalization community since 2025.
Rodolfo Soldati
Rodolfo is a postdoctoral fellow at the Institute for Quantum Computing, Waterloo, and
associate member at the Perimeter Institute. He has a joint PhD in quantum thermodynamics from the
Universities of Stuttgart, and of São Paulo. Since 2024, he has been involved in formalizing the
physics of quantum information in Lean.
Joseph Tooby-Smith
Joseph is lecturer (Assistant Professor) in computer science at the University of Bath.
He has a PhD in theoretical particle physics at the University of Cambridge.
He has been in the formalization community since 2023.
Winston Yin
No summary available.
Get Involved
Physlib is a community project. There are many ways to contribute — whether you're a physicist, a Lean enthusiast, or both.