Michael Rothgang’s homepage
About me
I’m a postdoctoral researcher in formalisation of mathematics at Universität Bonn. I work with Floris van Doorn on the formalisation of analysis and symplectic geometry.
I was a PhD student with Chris Wendl at Humboldt-Universität zu Berlin. Throughout my master's and PhD studies, I was a member of the Berlin Mathematical School (BMS). Before coming to Berlin, I obtained my undergraduate degree at Jacobs University Bremen.
My work on formalisation of mathematics concerns symplectic geometry and its foundations in a broad sense. This includes various topics in analysis and topology. In symplectic geometry, I am interested in equivariant transversality problems using holomorphic curves.
How to contact me
Office: Endenicher Allee 62, 53115 Bonn, room 1.001 (first floor)
Email: rothgang at math.uni-bonn.de.
Research interests
I work on formalising mathematics using the Lean theorem prover and the mathlib mathematical library. I have reviewer rights within mathlib. My current and past formalisation projects include
- contributing to the Carleson project,
- formalising Sard's theorem (and Moreira's generalisation of it),
- formalising the foundations of bordism theory,
- the mathlib review dashboard.
In my PhD thesis, I studied equivariant transversality for closed holomorphic curves: given a symplectic manifold with a symplectic group action, the moduli space of closed holomorphic curves (with respect to equivariant compatible almost complex structures) is generally not a smooth manifold or orbifold: after all, transversality and symmetry are famously incompatible. However, I proved that the moduli space still has a well-behaved structure as a stratified spaces. This allows recovering transversality in good cases. Generalising this to punctured holomorphic curves is work in progress.
Publications, preprints and theses
I have defended my PhD thesis Equivariant transversality for closed holomorphic curves in September 2024 (slides), and am currently making some last corrections for a final version.
If you are interested in seeing it right now, feel free to email me.Homotopy Hubbard trees for post-singularly finite exponential maps (joint with David Pfrang and Dierk Schleicher).
This paper grew out of my bachelor’s thesis at Jacobs University Bremen. In his PhD thesis, David Pfrang generalised this result to all post-singularly finite transcendental functions.
Ergodic Theory and Dynamical Systems, volume 43(1), pages 253–298, October 2021 (open access).My master’s thesis: Flexibility and symplectic fillability (August 2019, last revised November 2019).
I have been told (by fellow students in Berlin and elsewhere) that my master’s thesis has been rather helpful as a learning resource, hence I am making it available here.This is a revised version, incorporating the feedback of my thesis readers. There were substantial changes to the overall structure, but no significant changes to the mathematical content.
If you are coming here for this reason, chapters 2 and 3 are probably the most useful. Chapter 2 introduces Liouville and Weinstein domains, speaking about loose Legendrians, handle attachments and flexible Weinstein domains also. Chapter 3 reviews Hamiltonian Floer homology and proceeds to basic properties of symplectic homology. Enjoy!
Here is a 3-page summary of my thesis, aimed at a more advanced audience.Simulation and Visualization to Support Breast Surgery Planning (joint with J. Georgii, T. Paetz, M. Harz, C. Stoecker, J. Colletta, K. Schilling, M. Schlooz-Vries, R. Mann, and H. K. Hahn). In: Proceedings of the 13th International Workshop on Breat Imaging (IWDM 2016), pages 257–264.
My undergraduate internship at the Fraunhofer MEVIS institute in Bremen was on an applied project: extending a deformation simulation for breast tissue. This has uses in breast surgery planning: breast position during surgery (patient lies on their back) differs substantially from its positioning in radiological images. (During a mammography, the breast is compressed; during MRI imaging the patient lies face down.) Hence, imaging information about the lesion must be adapted to the surgery scenario. MEVIS had developed a finite-element model to simulate the deformation of the breast tissue. My project dealt with extending the model to incorporate the influence of Cooper’s ligaments; this work led to the paper above.
Research talks
- Upcoming: Equivariant transversality for holomorphic curves, symplectic geometry seminar, July 16th, 2025, Strasbourg
Formalising bordism theory: a test of mathlib's differential geometry library, Formalised mathematics group seminar, April 28, 2025, Bonn (slides)
Bordism theory is perhaps the simplest example of an extraordinary homology theory. Proving the Eilenberg-Steenrod axioms is particularly simple (unlike for e.g. singular homology). It is used e.g. in the proof of the Hirzebruch signature theorem, which is one ingredient for the existence of exotic spheres. I have been working on formalising the basics of (oriented) bordism theory: this is both beautiful mathematics and an interesting test of mathlib's differential geometry library. I will explain the main ideas, and speak about the insights and challenges from formalisation: as so often, finding the right definition is less obvious than it seems.
In the second part, I'll take a step back and speak about the challenges of making this material mathlib-ready. Doing so requires a conceptually correct definition of smooth embeddings (which naturally yields to smooth submanifolds) and the inverse function theorem. I will present current progress on all of these questions. (Each of these is a basic ingredient of basic differential geometry, hence are of independent interest.) No prior knowledge in differential geometry will be assumed.
Equivariant transversality for holomorphic curves, Symplectic geometry seminar in Bonn, April 17, 2025
Consider closed holomorphic curves in symplectic $G$-manifolds, with respect to a $G$-invariant almost complex structure. We should not expect the moduli space of such curves to be a manifold (after all, transversality and symmetry are famously incompatible). However, we can hope for a clean intersection condition: the moduli space decomposes into countably many disjoint strata which are smooth manifolds, whose dimensions are explicitly computable. I present this decomposition for simple curves, and indicate how to extend this to multiple covers. These are the first steps towards a well-behaved theory of equivariant holomorphic curves. This has applications to the 3-body problem and real Gromov-Witten theory.
Formalising bordism theory, Leaning in! workshop, March 13, 2025, Berlin (slides)
Bordism theory is perhaps the simplest example of an extraordinary homology theory. Proving the Eilenberg-Steenrod axioms is particularly simple (unlike for e.g. singular homology). It is used e.g. in the proof of the Hirzebruch signature theorem, which is one ingredient for the existence of exotic spheres. I have been working on formalising the basics of (oriented) bordism theory: this is both beautiful mathematics and an interesting test of mathlib's differential geometry library. I will explain the main ideas, and speak about the insights and challenges from formalisation: as so often, finding the right definition is less obvious than it seems. This is ongoing work. No prior knowledge in differential geometry will be assumed.
Scaling mathlib: tooling and automation for an ever-growing mathematics library, Lean together 2025, January 16, 2025 (slides, video).
Maintaining the mathlib library in the presence of continuous growth is a challenge in many aspects. On a technical level, this relies on a fair amount of custom tooling and automation to keep things manageable. I will highlight some recent additions in areas such as deprecations, linting, bots and a new review dashboard. This involves work by many people, including Damiano Testa, Johan Commelin, Mario Carneiro and the author.
This talk is mostly aimed at mathlib contributors (and reviewers), but there will be useful information for mathlib users also.
Equivariant transversality for holomorphic curves, Geometry and Analysis Seminar at RWTH Aachen, November 15th, 2024
We study closed holomorphic curves in symplectic $G$-manifolds, with respect to a $G$-invariant almost complex structure. We should not expect the moduli space of such curves to be a manifold (after all, transversality and symmetry are famously incompatible). However, we can hope for a clean intersection condition: the moduli space decomposes into countably many disjoint strata which are smooth manifolds, whose dimensions are explicitly computable.
I present this decomposition for simple curves, and indicate how to extend this to multiple covers. These are the first steps towards a well-behaved theory of equivariant holomorphic curves. This has applications to the 3-body problem and real Gromov-Witten theory.
An invitation to formalising mathematics, BMS-BGSMath Junior Meeting, June 2024, Berlin (slides, handout version)
Are you wondering what the recent excitement about Lean is about? What the formalisation of deep theorems (such as the liquid tensor experiment, sphere eversion or the unit fractions project) means? Why we would be interested in doing this? I will answer all these questions and give an impression of the current state of things. There will also be some pointers to how to get involved.
An invitation to formalising mathematics, BMS Student Conference, February 2024 (slides, handout version)
See the above talk for the abstract.Equivariant transversality for holomorphic curves, Dynamics seminar at Ruhr-Universität Bochum, November 14th, 2023.
See the above talk in Aachen for an approximate abstract.Equivariant transversality for simple holomorphic curves, Symplectic geometry seminar at Universität Heidelberg, June 28th, 2023.
See the above talk in Aachen for an approximate abstract.- Holomorphic curves and the restricted three-body problem, Young researchers’ workshop Pseudoholomorphic Curves in Hamiltonian Dynamics, Heidelberg, March 2023.
A glimpse at symplectic geometry and pseudo-holomorphic curves (slides), BMS Student Conference, February 2023.
The mathematical treatment of classical mechanics naturally leads to symplectic geometry, the study of symplectic manifolds. Symplectic geometry has rich connections to various branches of mathematics, such as enumerative and algebraic geometry, functional analysis, elliptic partial differential equations and dynamical systems. We present some results illuminating these connections.
A fundamental tool for many of these connections are pseudo-holomorphic curves. We give an overview of their theory, discuss some fundamental questions which are still open and indicate some avenues for addressing them. No prior knowledge of symplectic geometry will be assumed.
Equivariant transversality for simple holomorphic curves, Symplectic geometry seminar at HU Berlin, November 2022
Consider a closed symplectic manifold with a compact Lie group $G$ acting symplectically. What can we say about the moduli space of holomorphic curves on $M$, w.r.t. a generic $G$-equivariant almost complex structure? We should not expect it to be a manifold (after all, transversality and symmetry are famously incompatible). However, we can hope for a clean intersection condition: the moduli space decomposes into disjoint strata which are smooth manifolds of explicitly computable dimension. I will focus on the case of simple curves (which is already surprisingly interesting): I'll explain how to decompose the moduli space into iso-symmetric strata and prove that each stratum is smooth.
Transversality for simple holomorphic curves and the slice theorem, Symplectic geometry seminar at HU Berlin, November 2022
I will review the necessary prerequisites for my talk next week. Firstly, I'll show that simple holomorphic curves are generically Fredholm regular; i.e. "transversality holds for simple curves". The proof is standard, but will become much more interesting in the equivariant case. Secondly, we will review the slice theorem for smooth Lie group actions on Banach manifolds --- with an eye towards infinite-dimensional applications. If time permits, we might see how these are related.
A glimpse at symplectic geometry and pseudo-holomorphic curves, BMS-BGSMath Junior Meeting 2022, September 2022.
Another talk to a general mathematical audience — leading up to the role of holomorphic curves in constructing symplectic invariants such as Hamiltonian Floer homology and symplectic homology (extended slides).Bai-Swaminathan I (Taubes’ Gromov invariant in Calabi-Yau 6-folds), Symplectic geometry seminar at HU Berlin, November 2021
It has long been conjectured that in symplectic Calabi-Yau 6-manifolds, there should exist an analogue of the Gromov invariant that gives integer-valued counts of embedded holomorphic curves, together with contributions from their multiple covers that are determined by bifurcation analysis. It is still an open question how to define such an invariant in general, but a recent preprint of Bai and Swaminathan explains how to do it in situations where the multiple covers making contributions have degree at most 2. This talk will give a general overview of the construction.
Isolated singularities, minimal discrepancy and exact fillability (Slides), Symplectic geometry seminar at HU Berlin, February 2021
We discuss isolated singularities in (affine) algebraic varieties and explore McLean's result that the minimal discrepancy of a sufficiently nice isolated singularity is closely related to a symplectic invariant. The crucial tool for this result is the link of a singularity, which is a contact manifold: the minimal discrepancy of a singularity can be computed in terms of Conley-Zehnder indices of Reeb orbits of its link. This is motivated by Zhou's recent results on exact non-fillability of projective spaces &emdash; they indicate that algebro-geometric properties of an isolated singularity are related to the filling properties of its link.
No prior knowledge of algebraic geometry will be assumed.Symplectic cohomology of Liouville sectors, part 2: algebraic constructions (Notes), Berlin-Hamburg-Augsburg symplectic geometry seminar, June 2020
About §4 in Ganatra-Pardon-Shende's paper.Form follows function’s flow: what does pouring honey on a lifebuoy have to do with planetary motion?, BMS Student conference 2020.
A general audience introduction of Morse and Hamiltonian Floer homology. Slides (pdf).The twisted bundle decomposition of Cauchy-Riemann operators with symmetry, Symplectic geometry seminar at HU Berlin, December 2019
This talk does not require significant knowledge of holomorphic curve theory or Cauchy-Riemann operators, but instead requires some standard facts about covering spaces and vector bundles, and bit of the representation theory of finite groups (e.g. orthonormality of characters). The goals are to explain (1) the canonical regular cover that is determined by any branched cover of Riemann surfaces, and how to identify its automorphism group; (2) why the normal Cauchy-Riemann operator of any multiply covered holomorphic curve has a natural direct sum decomposition with summands corresponding to the irreducible representations of the (generalized) automorphism group. This discussion culminates in a dimension formula (Corollary 3.21) that is crucial for computing the dimensions of the strata in the stratification theorem.
Part of the Berlin group seminar studying Wendl's paper Transversality and super-rigidity for multiply covered holomorphic curves.
Teichmüller slices, Fredholm regularity and the implicit function theorem, Symplectic geometry seminar at HU Berlin, October 2019
The main goals are to define the moduli space of closed unparametrized J-holomorphic curves in an almost complex manifold, the notion of Fredholm regularity for such curves, and prove the standard theorem endowing the (open) set of regular curves in the moduli space with the structure of a smooth finite-dimensional orbifold. Some facts about the moduli space of Riemann surfaces and Teichmüller space will also need to be mentioned, most likely without proof; the fact that the linearized Cauchy-Riemann operator is Fredholm should likewise be taken as a black box.
Part of the Berlin group seminar studying Wendl's paper Transversality and super-rigidity for multiply covered holomorphic curves.Hubbard trees for exponential maps, BMS Student conference 2017 (slides (pdf), video recording)
An expository talk about the Homotopy Hubbard trees paper above.
Teaching
I have taught a variety of courses at various institutions, both in German and English and in various roles — ranging from a student assistant to a Wissenschaftlicher Mitarbeiter.
- In summer 2024, Yves Jäckele, Nicolas Weiss and I organised a one-day workshop for learning Lean: see here for further information.
- Algebra und number theory (for math teacher students), summer term 2024, HU Berlin.
In German. Preparing and holding weekly tutorials, exam grading. - Geometrie (axiomatic geometry, for math teacher students), winter term 2023/24, HU Berlin.
In German. Preparing and holding weekly tutorials, exam grading. - Linear algebra and analytic geometry II, summer term 2020, HU Berlin.
In German. Preparing problem sheets, preparing and holding weekly tutorials, exam grading. - Linear algebra and analytic geometry I (for math teacher students), winter term 2019/20, HU Berlin.
In German. Preparing and holding weekly tutorials, exam grading. - Analysis II, summer term 2018, FU Berlin. In German.
Preparing and holding weekly tutorials, grading homeworks. - Algebra and number theory, winter term 2017/18, FU Berlin. In German.
Preparing and holding weekly tutorials, grading homeworks and exams. - Linear algebra (for computer science students), summer term 2017, FU Berlin. In German.
Preparing and holding weekly tutorials, grading homeworks and exams. - Stochastics (for math teacher students), winter term 2016/17, FU Berlin. In German.
Preparing and holding weekly tutorials, grading homeworks and exams. - Analysis II, spring term 2016, Jacobs University Bremen. In English.
Student assistant: homework and exam grading, holding tutorials. - Analysis I, autumn term 2015, Jacobs University Bremen. In English.
Student assistant: homework and exam grading, holding tutorials. - Modern Mathematics summer school, July 2015. In English.
Teaching assistant: holding tutorials to lectures for Matthias Görner and Rebecca Waldecker. - Linear algebra I, Jacobs University Bremen, autumn term 2014. In English.
Student assistant: grading of homework and holding office hours.