معرفی
Patrick Massot is a Professor in the Department of Mathematics at the Faculty of Sciences of Orsay, University of Paris-Saclay, France. His work bridges pure mathematics and formal verification, with a focus on symplectic and contact geometry, and the formalization of advanced mathematical theories using the Lean proof assistant.
His research interests include symplectic geometry, contact geometry, formalized mathematics, and differential topology. He has contributed significantly to the formalization of perfectoid spaces, the h-principle, and sphere eversion. His recent work emphasizes the educational use of proof assistants in teaching undergraduate mathematics.
The most recent publications reflect a strong trend toward formal verification in mathematics, combining geometric intuition with rigorous computational proof. These works span topics such as convex integration, holonomic approximation, and the use of Lean for pedagogy. The underlying themes include flexibility in geometry, foundational rigor, and interdisciplinary collaboration between mathematics and computer science.
- Program Committee Member, CPP 2025
- Author, Formalising the h-principle and sphere eversion (CPP 2023)
Patrick Massot has advised no publicly listed students, and no specific grants are mentioned. However, his collaborative work with prominent mathematicians (e.g., Buzzard, Commelin, Giroux, Etnyre) suggests active research funding and participation in major projects such as the Liquid Tensor Experiment.
He leads a formalized mathematics working group and was involved in a 2015–2016 working group on sheaf theory applied to Lagrangian submanifolds. These groups serve as hubs for collaborative research in formalization and geometric topology.
