Introduction: Jonathan Michala

Stream: new members

[Jonathan Michala]

Hey there! I'm currently at the Odyssey conference on theoretical AI alignment, and had a good conversation about Lean with @Alok Singh. My background is in symplectic geometry - I just finished my PhD in May at USC (now I work at MATS, an AI safety mentorship program). I first joined this zulip 2 or 3 years ago, when I thought I might have time to contribute to symplectic geometry in Mathlib. Unfortunately, I didn't end up making any contributions. I just wanted to reach out and see if now is the time to jump in. Is anybody here thinking about symplectic stuff?

[Michael Rothgang]

Hi and welcome! I'm a symplectic geometer by training; I completed my PhD (about equivariant pseudo-holomorphic curves) last September. Now, I'm a postdoc and have the privilege to work on mathlib. My dream and medium-term goal is to formalise the foundations of symplectic geometry: we'll get there, but there remains some work to do.

[Kevin Buzzard]

As far as I know we still don't have the definition of symplectic manifold? Do we even have a definition of 2-form??

[Michael Rothgang]

@Patrick Massot also has a background in symplectic geometry (he might say differential topology)

[Michael Rothgang]

@Heather Macbeth wrote a sneaky definition of symplectic manifolds: it's not mathlib-ready yet, but the pieces are slowly lining up. If you allow slight cheating, you can write the definition of 2-form today.

[Michael Rothgang]

The proper way is to define n-forms, which Sam Lindauer has been working on (with lots of help by Yury Kudryshov and advised by Johan Commelin). They made a lot of progress (https://github.com/urkud/DeRhamCohomology), but there's also quite a bit of work remaining --- and all of this needs to get merged into mathlib.

[Michael Rothgang]

This recent message of mine #new members > Bennett Chow @ 💬 has the current state of differential geometry in mathlib: there is a lot already present, and lots of opportunities to contribute further.

[Michael Rothgang]

In short: I'm always very happy about new faces who are interested in differential geometry. If you have questions about doing that in Lean, don't hesitate to ask! And if you're looking for some project, but need an idea, I have more project ideas than time - so am happy to suggest something (or to collaborate on a project, which is usually more fun than doing things alone)!

[Michael Rothgang]

One symplectic project that could be fun would be to define almost complex structures, and formalise Sévennec's proof that the space of tame almost complex structures is contractible. (It's probably easiest to restrict to tame ones, and over a single point, i.e. on a vector space --- one difficulty at a time.)
You probably need to define the weak topology on C^k maps between manifolds, though --- I believe mathlib has the compact-open topology (for continuous maps), but nothing for higher smoothness.

[Jonathan Michala]

Thanks for the reply @Michael Rothgang ! Would be great to chat more at some point. I'll take a look at the n-form github and the Bennett Chow thread. The almost complex structure project sounds cool!