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.
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:
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.