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 FSMP 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.
Publications and preprints
Anatomy of a formal proof. With Jeremy Avigad, Johan Commelin and Adam Topaz. To appear in Notices of the American Mathematical Society.
The Mechanics of Proof, an introduction-to-proof text, "bilingual" between English and the computer formalization language Lean.
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, the New York Timescovered some different aspects in 2023; 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:
The Arnold chord conjecture. Part III essay, Cambridge, 2010, written under the supervision of Gabriel Paternain.
Teaching highlights
In Fall 2024 (upcoming), Spring 2024, Fall 2023 and Spring 2023 I taught a new version of Fordham's MATH 2001 (Discrete Mathematics), incorporating numerous exercises in the proof assistant Lean. Here is a draft textbook I am developing from the lecture notes and here is the course's Lean code on GitHub.
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.
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.
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 2023 on a National Academies webinar on "Artificial Intelligence to Assist Mathematical Reasoning," and 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.
