Patrick Massot

Patrick Massot is a mathematician who moved from contact geometry to formalized mathematics, working with the Lean proof assistant and its Mathlib library. He earned a PhD at École Normale Supérieure de Lyon in 2008 and began using Lean in 2017. With Kevin Buzzard and Johan Commelin he posted Formalising perfectoid spaces in 2019, and with Floris van Doorn and Oliver Nash he posted Formalising the h-principle and sphere eversion in 2022. He received a Microsoft Research Lean Award in 2023, published the Verbose Lean teaching library in 2024, and spoke at the Workshop on AI and Theorem Provers in Mathematics in 2026. He is a professor at the Laboratoire de Mathématiques d'Orsay of Université Paris-Saclay, a Mathlib maintainer and a co-author of Mathematics in Lean.

Now at: Université Paris-Saclay
Works: 31
Citations: 309
h-index: 10
Badges: Wayfarer

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

2008–2012

A Lyon doctorate in contact geometry

He earns a PhD at École Normale Supérieure de Lyon in 2008 under Emmanuel Giroux, with a dissertation on Riemannian properties of contact structures in dimension three. In 2012, Inventiones Mathematicae publishes Tightness in contact metric 3-manifolds, written with John Etnyre and Rafał Komendarczyk.
2017

First steps with Lean

In 2017, he starts using Lean to check his computations, becomes interested in formalized mathematics, and quickly sees the potential of the proof assistant.
2019–2021

Perfectoid spaces and liquid tensor

In October 2019, he posts Formalising perfectoid spaces with Kevin Buzzard and Johan Commelin; the three formalize in Lean enough definitions and theorems to define perfectoid spaces, which Peter Scholze introduced in 2012. In May 2021, he is among the Lean community members who help complete the formal proof of Theorem 9.4, the first target of Scholze's liquid tensor experiment.
2022

Sphere eversion in Lean

In October 2022, he posts Formalising the h-principle and sphere eversion with Floris van Doorn and Oliver Nash. The paper describes a Lean formalization of the local h-principle for first-order, open, ample partial differential relations. The sphere eversion project he builds with Nash and van Doorn aims to show that the proof assistant can handle geometric topology.
2023

A Microsoft Research Lean Award

He receives a Microsoft Research Lean Award for the 2023 academic year, given to mathematicians who emerged as leaders in the Lean community. The award funds a one-year postdoctoral position in Orsay on formalization of mathematics.
2024

Verbose Lean for teaching

In 2024, the International Conference on Interactive Theorem Proving publishes his paper Teaching Mathematics Using Lean and Controlled Natural Language, which presents Verbose Lean, a library that teaches undergraduate students to read and write traditional paper proofs. In May 2024, he gives a Cambridge talk on teaching first-year students with Lean, listed under Université Paris-Saclay and Carnegie Mellon University.
2025–2026

Lean meetings and AI workshops

In August 2025, he gives the lecture Why explain mathematics to computers?, which touches on links with AI. In January 2026, he is one of four main organizers of Lean Together 2026, a virtual meeting for Lean users and developers. In April 2026, he speaks on teaching with Verbose Lean at the Workshop on AI and Theorem Provers in Mathematics.
As of October 2026

Professor at Orsay

He is a professor at the Laboratoire de Mathématiques d'Orsay of Université Paris-Saclay, where his research covers contact and symplectic geometry and formalized mathematics in Lean. He is a Mathlib maintainer and works with Jeremy Avigad on the Mathematics in Lean textbook.