Bulhwi Cha & Seongwoo Shim: Introductions

Stream: new members

[shimsw20]

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]

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]

note that this is all in Lean 3

[shimsw20]

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

[Matej Penciak]

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]

@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]

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

[Matej Penciak]

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]

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]

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

[Bulhwi Cha]

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.