PeopleofSuperintelligence

Researcher

Oliver Nash

Oliver Nash is a mathematician who formalizes mathematics in Mathlib and co-authored a Nature paper on formal mathematical reasoning with reinforcement learning. He completed a DPhil in differential geometry at Oxford in 2006, with a dissertation on monopole moduli spaces. He began formalizing mathematics in 2019, and he posted Formalising Lie algebras in 2021, Formalising the h-principle and sphere eversion in 2022, and Engel's theorem in Mathlib in 2023. In September 2025, he interviewed Kevin Buzzard and Alex Kontorovich about Mathlib. As of October 2026, he is a senior manager at the Mathlib Initiative.

Now at
Mathlib Initiative
Works
15
Citations
94
h-index
6

Publication numbers from OpenAlex, as of 15 October 2026.

Timeline

  1. 2006

    A DPhil on monopole moduli spaces

    He completes a DPhil in differential geometry at Oxford in 2006, with a dissertation on monopole moduli spaces.

  2. Since 2019

    Formalizing mathematics

    He starts formalizing mathematics in 2019.

  3. December 2021

    Formalising Lie algebras

    He submits Formalising Lie algebras to arXiv in December 2021, a report on Lie algebras in Mathlib.

  4. October 2022

    Formalising sphere eversion

    In October 2022, he and two co-authors post Formalising the h-principle and sphere eversion, which describes a Lean formalisation of the local h-principle.

  5. April 2023

    Engel's theorem in Mathlib

    In April 2023, he posts Engel's theorem in Mathlib, where all arguments work with coefficients in any commutative ring.

  6. September 2025

    Interviews about Mathlib

    In September 2025, he separately interviews Kevin Buzzard and Alex Kontorovich about Mathlib and the Mathlib Initiative.

  7. November 2025

    A Nature paper on formal reasoning

    In November 2025, Nature publishes Olympiad-level formal mathematical reasoning with reinforcement learning, which lists him among its authors.

  8. As of October 2026

    Senior manager at the Mathlib Initiative

    As of October 2026, he is a senior manager at the Mathlib Initiative.

Sources and credits

Photo: We have no published photo of Oliver Nash yet. Send us a free-licensed photo.

  1. Mathlib maintainers leanprover-community.github.io. Checked 15 October 2026.
  2. Oliver Nash - The Mathematics Genealogy Project mathgenealogy.org. Checked 15 October 2026.
  3. [math/0610295] Differential geometry of monopole moduli spaces arxiv.org. Checked 15 October 2026.
  4. [2112.04570] Formalising Lie algebras arxiv.org. Checked 15 October 2026.
  5. [2210.07746] Formalising the $h$-principle and sphere eversion arxiv.org. Checked 15 October 2026.
  6. [2304.10424] Engel's theorem in Mathlib arxiv.org. Checked 15 October 2026.
  7. Kevin Buzzard and Alex Kontorovich on the Future of Formal Mathematics: A Mathlib Initiative Interview renaissancephilanthropy.org. Checked 15 October 2026.
  8. Olympiad-level formal mathematical reasoning with reinforcement learning nature.com. Checked 15 October 2026.