Hamiltonian Mechanics

Stream: Natural sciences

[Lehel Csillag]

Hey everyone. I am a mathematical physics student completely new to lean, and would like to learn more about what has already been done. I would like to formalize Hamiltonian Mechanics (in the language of symplectic geometry) in Lean. How/where could I start? Are basics of symplectic geometry/ODE/PDE theory formalized already?

[Lehel Csillag]

(deleted)

[Notification Bot]

A message was moved here from #Natural sciences > physical units by Eric Wieser.

[Patrick Massot]

We are still pretty far away from this. Differential forms are very close but not there yet. ODE theory has the fundamental existence of uniqueness result but not much more. PDE has nothing basically. There is a huge imbalance in the Lean user community between algebraic geometry and the rest of the world.

[Tyler Josephson ⚛️]

We’re really interested in this too! But still learning, as we come from an engineering background and not mathematics. Would love to see progress along these lines. @Bulhwi Cha is another person who’s looked into this.

[Bulhwi Cha]

I'm currently focusing more on game development than formalizing mathematics. I need to make money first. But I'll find time to formalize these theories later.

[Eric Wieser]

Patrick Massot said:

There is a huge imbalance in the Lean user community between algebraic geometry and the rest of the world.

Is this to say that we are biased quite heavily towards it, or away from it?

[Matthew Ballard]

I mean look how much time lean _lovingly_ spends building AG :)

[Patrick Massot]

Eric, I meant there are a lot more people doing algebraic geometry here than in the real world, in proportion.

[Kevin Buzzard]

Just to further clarify: Patrick doesn't even mean "as a proportion of all human beings" (for which the claim is self-evident), he means "as a proportion of people working in maths departments". The community is very skewed here because people were attracted by flagship projects which mostly were on the more algebraic geometry side of things.