Maintainers

The following individuals are the maintainers of this project. They are the people who have the power to approve the merger of pull requests, and who have 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.