Researcher

Heather Macbeth

Heather Macbeth is a mathematician at Imperial College London who works in Kähler geometry and helps maintain Mathlib, the library of formalized mathematics for the Lean proof assistant. After studying at Auckland and Cambridge, she earned a Princeton PhD under Gang Tian in 2015 and held posts at MIT and the École Normale Supérieure. In 2019 she tried a proof assistant for the first time and joined Fordham University, and she became a Mathlib maintainer in 2020; her Lean work includes semilinear maps for functional analysis and The Mechanics of Proof, a textbook paired with Lean code. In 2023 she sat on the National Academies committee that planned a workshop on artificial intelligence to assist mathematical reasoning, and in April 2025 she spoke at ICERM's workshop on autoformalization. Today she is a senior lecturer in pure mathematics at Imperial, on leave from Fordham.

Timeline

  1. 2006–2015

    Auckland, Cambridge and Princeton

    She studies as an undergraduate at the University of Auckland from 2006 to 2009 and takes Part III at Trinity College, Cambridge, from 2009 to 2010. She completes a PhD at Princeton University in 2015 under the supervision of Gang Tian.

  2. 2015–2019

    Postdocs at MIT and the ENS

    She is a C. L. E. Moore Instructor at MIT from 2015 to 2018 and an FSMP postdoc at the École Normale Supérieure from 2018 to 2019. In 2019, she tries a proof assistant for the first time, Coq, and begins formalizing mathematics.

  3. 2019–2020

    Joining Fordham and Mathlib

    She becomes an assistant professor at Fordham University in 2019 and a Mathlib maintainer in 2020, working on formalization projects in analysis and geometry. In an October 2020 Quanta Magazine feature on Mathlib, she predicts it will likely be decades before Lean is a research tool.

  4. 2022

    Semilinear maps in Mathlib

    With Frédéric Dupuis and Robert Y. Lewis, she implements semilinear maps in Lean's Mathlib library and presents the work at the 2022 International Conference on Interactive Theorem Proving. The project formalizes the Fréchet–Riesz representation theorem and the spectral theorem for compact self-adjoint operators over real and complex Hilbert spaces.

  5. 2023

    A Microsoft Research Lean Award

    She receives a Microsoft Research Lean Award for the 2023 academic year to support formalizing the foundations of partial differential equations, a new undergraduate Fordham course using Lean, and Mathlib maintenance. Her textbook The Mechanics of Proof, written for Fordham's Math 2001 course, pairs rigorous proof writing with code in Lean.

  6. 2023–2024

    National Academies AI workshop

    In 2023, she serves on the National Academies planning committee for a workshop on artificial intelligence to assist mathematical reasoning, with Terence Tao among its members. In May 2024, she posts "Algorithm and abstraction in formal mathematics", an invited lecture for the 2024 International Congress on Mathematical Software that analyses style in prose and computer-formalised mathematics.

  7. 2025

    Talks on autoformalization and geometry

    In April 2025, she presents "Proofs and the tools they use" at ICERM's workshop Autoformalization for the Working Mathematician. In May 2025, she speaks for Imperial College London at Oxford's Geometry and Analysis Seminar on the state of the art in formalising geometry.

  8. As of October 2026

    Senior lecturer at Imperial

    She is a senior lecturer in pure mathematics at Imperial College London, working in Kähler geometry and geometric analysis, and is on leave from Fordham, where she is an associate professor. She also serves on Mathlib's admin team and has written some 16,000 lines of code for the library.

Sources and credits

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

  1. Heather Macbeth ma.imperial.ac.uk. Checked 19 October 2026.
  2. SMY:n etäkollokvio ke 18.10. | Suomen matemaattinen yhdistys matemaattinenyhdistys.fi. Checked 19 October 2026.
  3. Building the Mathematical Library of the Future | Quanta Magazine quantamagazine.org. Checked 19 October 2026.
  4. Mathlib maintainers leanprover-community.github.io. Checked 19 October 2026.
  5. Microsoft Research Lean Award Program - Microsoft Research microsoft.com. Checked 19 October 2026.
  6. [2202.05360] Formalized functional analysis with semilinear maps arxiv.org. Checked 19 October 2026.
  7. The Mechanics of Proof — The Mechanics of Proof, by Heather Macbeth hrmacbeth.github.io. Checked 19 October 2026.
  8. Read "Artificial Intelligence to Assist Mathematical Reasoning: Proceedings of a Workshop" at NAP.edu nationalacademies.org. Checked 19 October 2026.
  9. [2405.04699] Algorithm and abstraction in formal mathematics arxiv.org. Checked 19 October 2026.
  10. Proofs and the tools they use | MathInstitutes.org mathinstitutes.org. Checked 19 October 2026.
  11. The state of the art in the formalisation of geometry | Mathematical Institute maths.ox.ac.uk. Checked 19 October 2026.
  12. Heather Macbeth | Fordham University faculty.fordham.edu. Checked 19 October 2026.