Heather Macbeth

Heather Macbeth

Department of Mathematics
Fordham University

Office: LL 819C
Email: hmacbeth1 at fordham dot edu

I am an assistant professor at Fordham University, with research interests in Kähler geometry and in geometric analysis. In the last few years I have also become very interested in the formalization of mathematics.

Before Fordham I was a Fondation Sciences Mathématiques de Paris postdoc (2018-19) at the Ecole Normale Supérieure. Before the ENS I was a C. L. E. Moore Instructor (2015-18) at MIT. Before MIT I was a graduate student (2010-15) at Princeton, under the supervision of Gang Tian. Before Princeton I was a Part III student (2009-10) at Trinity College, Cambridge. Before Cambridge I was an undergraduate (2006-9) at the University of Auckland.

Preprints and recent publications

  • Formalized functional analysis with semilinear maps. With Frédéric Dupuis and Robert Y. Lewis. 13th International Conference on Interactive Theorem Proving, 10:1-10:19, 2022. [arXiv] [code]
  • Steady Kähler-Ricci solitons on crepant resolutions of finite quotients of Cn. With Olivier Biquard. Preprint, 2017.
  • Kähler-Einstein metrics and higher alpha-invariants. Preprint, 2014.
  • Conformal classes realizing the Yamabe invariant. International Mathematics Research Notices 2019 (2019), no. 5, 1333-1349. [arXiv] [MR]
  • Detecting Einstein geodesics: Einstein metrics in projective and conformal geometry. With Rod Gover. Differential Geometry and its Applications 33 (2014), suppl., 44-69. [arXiv] [MR]
  • Einstein metrics in projective geometry. With Andreas Čap and Rod Gover. Geometriae Dedicata 168 (2014), 235-244. [arXiv] [MR]
  • Older publications

  • Cayley graphs of given degree and diameter for cyclic, Abelian, and metacyclic groups. With Jana Šiagiová and Jozef Širáň. Discrete Mathematics 312 (2012), no. 1, 94-99. [MR]
  • Cayley graphs and vertex-transitive non-Cayley graphs of given degree and diameter. With Jana Šiagiová, Jozef Širáň and Tomáš Vetrík. Journal of Graph Theory 64 (2010), no. 2, 87-98. [MR]
  • Code

    I am a contributor to and maintainer of the mathematics formalization library mathlib for the Lean proof assistant. I also serve on the admin team for the project as a whole. (What is this all about? Quanta ran a nice survey in 2020, here's a talk I gave in 2023 at IPAM on aspects of the project's philosophy.)

    I have written some 16,000 lines of code for mathlib, and substantially rewritten several thousand more. You can get a sense of my work on the project from the list of files in the library authored or co-authored by me, ranging from boilerplate to graduate-level analysis and differential geometry. My Github user page has a chronological overview which also includes my activity reviewing others' contributions. The webpage for my article with Frédéric Dupuis and Rob Lewis also has detailed links to the code for that article.

    As a sample of other work, here is the culminating file in each of several sequences of contributions:
  • Smooth vector bundles
  • Fourier series, also see a talk from April 2022
  • The area of a circle, undergraduate project by James Arthur, Benjamin Davidson and Andrew Souther, also see a talk from March 2021
  • Manifold structure on the sphere, also see a talk from January 2021
  • Some expository writings

  • Classification of one-dimensional isocrystals, blog post (with Rob Lewis)
  • Algebraic computations in Lean. Notes for a tutorial on Lean-Sage interaction, ICERM, 2022. (There is also a videorecording.)
  • Plongements des tores plats, by Daheng Min and Ivan Yakovlev. Undergraduate project, ENS, 2019.
  • Le problème de Yamabe. Notes for a talk in the "Raconte-moi" seminar, ENS, 2018.
  • An introduction to equivariant cohomology and the equivariant first Chern class, by YiYu (Adela) Zhang. Undergraduate project, MIT, 2017.
  • A compactness theorem for Yamabe metrics
  • Explicit constants for Riemannian inequalities
  • Moduli spaces of Einstein metrics. Notes for a talk in the Graduate Student Seminar, Princeton, 2011.
  • The Arnold chord conjecture. Part III essay, Cambridge, 2010, written under the supervision of Gabriel Paternain.

    Teaching highlights

  • In Spring 2023 I taught a new version of Fordham's MATH 2001 (Discrete Mathematics), incorporating numerous exercises in the proof assistant Lean. Here are the lecture notes and here is the course's Lean code on GitHub. Feedback and experimentation welcome, whether you are a student enrolled in the course or just a passer-by!
  • In Spring 2022 (Fordham MATH 4020) and Fall 2016 (MIT 18.950) I taught a course on elementary differential geometry; my version of this course introduces geodesics early and emphasizes explicit examples.
  • In the academic years 2021-22 and 2020-21 I taught the math portion of the Fordham honors sequence HPLC 1603-4. This is meant to be a concepts-based, low-computation course with no prerequisites. I covered phase-portrait analysis of dynamical systems, with examples drawn from natural science; turtle graphics programming; numerical analysis of dynamical systems; and optimization algorithms.
  • In Spring 2020 I taught Fordham's MATH 3005 (Abstract Algebra); my version of this course has extensive coverage of matrix groups and the Euclidean group, and illustrates many concepts using Cayley graphs.
  • In Spring 2018 I was the lead instructor, and in Spring 2017 I was the writing instructor, for 18.100P, a new MIT course, aimed at double- and non-majors, which covers elementary real analysis while developing mathematical writing skills. Materials I wrote for this course included some fun multi-week projects exploring applications of real analysis to physics, computer science, economics, etc.


    I was the recipient of a 2022 Microsoft Research Lean Award.

    Workshops, etc.

  • AI to Assist Mathematical Reasoning, workshop, NASEM (committee, with Petros Koumoutsakos, Jordan Ellenberg, Melvin Greer, Brendan Hassett, Yann LeCun, Talia Ringer, Kavitha Srinivas, Terence Tao)
  • Formalization of Mathematics graduate summer school, June 2023, SLMath (formerly MSRI), Berkeley (organizer, with Jeremy Avigad, Patrick Massot)
  • Formalization of Cohomology Theories, May 2023, BIRS, Banff (organizer, with Adam Topaz, Anne Baanen, Matthew Ballard, Johan Commelin)
  • Lean for the Curious Mathematician 2022, July 2022, ICERM, Providence (organizer, with Jeremy Avigad, Kevin Buzzard, Johan Commelin, Yury Kudryashov, Scott Morrison). A reflection on this workshop was featured on the NSF Mathematical Sciences Institutes website.
  • Fordham colloquium-style seminar (2020-21 organizer, with Han-Bom Moon)

    and some outreach work: I have served on the selection committee for the Fordham Clare Boothe Luce scholarships; female math majors at Fordham should definitely apply for this! I spoke in 2022 at the Microsoft Research Summit. I have taught, mentored and graded extensively for the NZMOC (and less extensively for the BMOC and the USAMO), most recently at a 2022 NZMOC camp for female and non-binary students. I helped organise a math afternoon for high school students at the ENS in 2019. I served on the MIT math department's Diversity Committee. I organized the Princeton Noetherian Ring for two years. I have asked and answered some questions at MathOverflow.