Joël Riou

Timeline

1. 2006

   A mathematics doctorate

   He earns a mathematics doctorate at Université Paris VII in 2006, with Bruno Kahn directing his thesis through the number theory team at the Institut de Mathématiques de Jussieu.

2. September 2007

   A faculty post at Paris 11

   In September 2007, he joins Université Paris 11 as maître de conférences in its Arithmetic and Algebraic Geometry team.

3. 2009–2010

   Algebraic K-theory and Riemann–Roch

   He posts his paper in 2009, showing how SGA 6 and A¹-homotopy theory lead to results in higher algebraic K-theory, Chern characters and Riemann–Roch. The Journal of Topology publishes it in 2010.

4. Since 2021

   Formalizing mathematics in Lean

   He begins formalizing mathematics in Lean in 2021.

5. January 2025

   AI and mathlib proof gaps

   In January 2025, he says some unfinished mathlib proofs require specific mathematical arguments that he would not expect AI to solve.

6. February 2025

   Freyd–Mitchell in mathlib

   He contributes formalizations of the small object argument and enough injectives for Grothendieck abelian categories. The Freyd–Mitchell embedding theorem enters mathlib in February 2025, with the enough-injectives result as a key ingredient.

7. July 2025

   Derived categories in Lean/mathlib

   In July 2025, he publishes a formalization of derived categories in Lean/mathlib. The paper models the derived category of any abelian category as a localization of unbounded cochain complexes and gives it a triangulated structure.

8. As of October 2026

   Associate Professor and Mathlib maintainer

   He is an Associate Professor of Mathematics at Université Paris-Saclay at Orsay and a Mathlib maintainer. In April 2026, he presents Lean work on verifying Quillen’s axioms of model categories for topological spaces and simplicial sets. With Fabrice Orgogozo, he publishes a 2026 paper on the characteristic cycle on a curve’s symmetric power and the determinant of étale cohomology.