# Zulip Chat Archive

## Stream: new members

### Topic: Bulhwi Cha & Seongwoo Shim: Introductions

#### shimsw20 (Aug 17 2022 at 13:56):

Nice to meet you all. My name is Seongwoo Shim, and I'm a Master's student in aerospace engineering at Seoul National University. My research interests include designing non-traditional aircraft such as Urban Air Mobility (UAM). I'm also interested in tensor analysis.

I set a goal of formalizing Lagrangian and Hamiltonian mechanics in Lean. If I succeed, I hope to formalize other engineering subjects: mechanics of materials, thermodynamics, fluid dynamics, electromagnetics, and aerodynamics.

#### Moritz Doll (Aug 17 2022 at 14:45):

I can comment a bit about Hamiltonian mechanics: the correct way of formalizing that is through symplectic geometry (in a sense symplectic geometry is Hamiltonian mechanics). The geometry part has the problem that the theory of manifolds is not far enough yet. On the other hand, there is symplectic linear algebra (symplectic forms, the various subspaces of sympletic vector spaces, symplectic transformations, etc) and this is very much feasible. For instance the definition of the sympletic matrices was formalized by @Matej Penciak and @Fabien Cléry recently #15513 (I might have helped a bit). For the abstract theory the starting point would be to look at this file https://leanprover-community.github.io/mathlib_docs/linear_algebra/sesquilinear_form.html but if you want to contribute to mathlib in that direction please check with Matej first, I don't know what he is up to and whether he has code for that stuff.

#### Moritz Doll (Aug 17 2022 at 14:48):

note that this is all in Lean 3

#### shimsw20 (Aug 19 2022 at 09:18):

Thanks for your advice. We'll first look into Mathlib APIs for linear algebra and geometry of manifolds.

#### Matej Penciak (Aug 22 2022 at 15:36):

Hey! Sorry for not responding earlier, I've been in the middle of moving between cities and was unable to access my computer for a while.

As @Moritz Doll mentioned, though the geometry might not be there yet to do symplectic **geometry** there's a ton of symplectic linear algebra that hasn't been done yet! I'm hoping to start tackling some of these topics now that I have more time again, but we can coordinate and work together if you are interested!

#### Bulhwi Cha (Aug 23 2022 at 13:46):

@Matej Penciak I'd love to participate in this, but @shimsw20 and I are afraid we might not be of much help because we lack a strong background in mathematics.

#### Bulhwi Cha (Aug 23 2022 at 13:54):

I should probably start learning prerequisites for symplectic linear algebra. Seongwoo is reviewing Lagrangian mechanics.

#### Matej Penciak (Aug 23 2022 at 17:25):

I'm not sure if this is the best reference, but I like the first couple sections of Ana Cannas da Silva's symplectic geometry book: https://people.math.ethz.ch/~acannas/Papers/lsg.pdf

I think having the definitions of coisotropic, isotropic, and Lagrangian subspaces together with some of their basic properties would be really great.

#### Moritz Doll (Aug 23 2022 at 17:41):

I think that that book is great, it assumes familiarity with manifolds, but it is possible to look only at the linear algebra part (first section + homework 1).

fun fact: in the intro Cannas da Silva thanks Allan Knutson who was at Lean for the curious mathematician at ICERM.

#### Patrick Massot (Aug 23 2022 at 19:15):

Yes, that book is very nice for elementary aspects of symplectic geometry (by elementary I mean the whole book).

#### Bulhwi Cha (Aug 24 2022 at 04:06):

I see. Then I guess I can try looking into this book. I'll make a new branch in Mathlib when I'm ready to formalize some definitions in the book.

Last updated: Dec 20 2023 at 11:08 UTC