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
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
- Heather Macbeth
- SMY:n etäkollokvio ke 18.10. | Suomen matemaattinen yhdistys
- Building the Mathematical Library of the Future | Quanta Magazine
- Mathlib maintainers
- Microsoft Research Lean Award Program - Microsoft Research
- [2202.05360] Formalized functional analysis with semilinear maps
- The Mechanics of Proof — The Mechanics of Proof, by Heather Macbeth
- Read "Artificial Intelligence to Assist Mathematical Reasoning: Proceedings of a Workshop" at NAP.edu
- [2405.04699] Algorithm and abstraction in formal mathematics
- Proofs and the tools they use | MathInstitutes.org
- The state of the art in the formalisation of geometry | Mathematical Institute
- Heather Macbeth | Fordham University
