Introduction: Wolfgang Schmaltz

Stream: new members

[Wolfgang Schmaltz]

Hi everyone!

My name is Wolfgang Schmaltz. I am a researcher in sympletic geometry, polyfold theory, and Gromov-Witten theory.

To tell you all a bit about my mathematical background...

To varying degrees, sympletic geometry has had issues with the rigor in its foundations (you could check this article for a general overview of one such situation).

I became interested in polyfold theory, developed by Hofer, Wysocki, and Zehnder. It was designed to give a firm foundation to the study of J-holomorphic curve moduli spaces and to give well-defined invariants of symplectic manifolds. I used polyfold theory to give a complete proof of the Gromov-Witten axioms (see here for an overview of my research).

Given my interest in rigorous mathematics, it has been very interesting to start learning about and using lean! I am especially impressed with the technical groundwork and tooling which make it possible to get real time feedback on the proof writing process. I am also impressed by the community adoption and support in developing mathlib.

Kudos to everyone involved :)

[Michael Rothgang]

Hi and welcome! As a (former?) symplectic geometer myself (did my PhD with Chris Wendl, and moved to Bonn for a postdoc in formalisation), I'm extremely happy to see more people interested in both symplectic geometry and formalisation. There are many things to do in symplectic geometry, so more help is certainly welcome.

I have been loosely following your polyfold work for a while, getting towards the point where we could even state some of this in Lean will take a while, but would be a great milestone. My personal medium-term target is defining J-holomorphic curves and perhaps a basic results such as Gromov's non-squeezing theorem, with everything this includes.

[Michael Rothgang]

Differential geometry in mathlib is at an interesting point, where many exciting developments are just around the corner, but not included in mathlib yet. I hope this will change a bit in the next few months. In the mean-time, I'm always happy to brainstorm ideas for useful targets towards symplectic geometry.