Sébastien Gouëzel
Also known as Sebastien Gouezel
Sébastien Gouëzel is a mathematician who works on dynamical systems and builds machine-checked proofs in Lean. He studied at the École normale supérieure in Paris from 1998 to 2002 and earned his PhD in mathematics in 2004 under Viviane Baladi. He began formalizing mathematics in 2016, first in Isabelle and then in Lean, and he is now one of the Mathlib maintainers. In 2019 he won the Brin Prize for work on the spectral theory of transfer operators and on hyperbolic dynamical systems. He is a first-class research director at CNRS, University of Rennes, a post held since 2021.
- Now at
- CNRS and University of Rennes
- Works
- 114
- Citations
- 2,381
- h-index
- 28
Publication numbers from OpenAlex, as of 15 October 2026.
Timeline
-
1998–2002
First place in the agrégation
He studies at the École normale supérieure in Paris from 1998 to 2002. In 2000 he places first in the agrégation in mathematics.
-
2001
Top of his DEA class
In 2001 he completes his DEA, a master's degree in pure mathematics, ranking first in his class.
-
2004
A PhD under Viviane Baladi
He earns his PhD in mathematics in 2004 under Viviane Baladi.
-
2014
A local limit theorem
In 2014 he publishes a local limit theorem for symmetric random walks in Gromov-hyperbolic groups.
-
2016
Formal proofs in Isabelle and Lean
He begins formalizing mathematics in 2016, first in Isabelle and then in Lean, a theorem prover in which a computer checks each proof against the rules of logic. He is now one of the Mathlib maintainers.
-
2019
The Brin Prize
He wins the Brin Prize in 2019 for work on the spectral theory of transfer operators and on hyperbolic dynamical systems.
-
Since 2021
A first-class research director
He is a first-class research director at CNRS, University of Rennes, a post held since 2021.
Sources and credits
Photo: We have no published photo of Sébastien Gouëzel yet. Send us a free-licensed photo.