Structure and Interpretation of Classical Mechanics

Stream: PhysLean

[Mark Ettinger]

Is anyone aware of any projects to translate Sussman's "Structure and Interpretation of Classical Mechanics" or "Functional Differential Geometry" into Lean from the original Scheme? There is (was?) a significant project to translate to Clojure but it seems me that a statically typed language like Lean would make the concepts more clear.

[Nicola Bernini]

That’s interesting. Just to clarify what direction you have in mind:
there seem to be (at least) two possible goals for such a translation.

1. A ​semantics / proof-oriented formalization​, closer to mathlib/PhysLean, where the main aim is verified definitions and theorems.
2. A more computation-oriented / symbolic reconstruction of the SICM machinery (closer in spirit to the original Scheme/Clojure systems), with execution and algebraic manipulation as the primary use case.

Lean can support both, but the design choices are quite different.
Which of these were you thinking of (or some hybrid)?

[Joseph Tooby-Smith]

I don't know any project translating Sussman.

In PhysLean we have bits of an API around classical mechanics, and some specific examples. Though there is lots more to be done in building up this API up. One approach talked about was to formalize the mechanics book of Landau and Lifshitz (see #PhysLean > Formalizing Landau and Lifshitz , but there were also lots of dicussion in one of the "PhysLean cafe's").

[Mark Ettinger]

I was thinking of the computational approach, in line with the original book.

[Joseph Tooby-Smith]

Out of interest, why Lean then and not something like Haskell?

[Mark Ettinger]

I think Haskell would be fine as I don't think one would need dependent types, though I'm not positive. I just like Lean.

[Joseph Tooby-Smith]

Makes sense :slight_smile:

[Joseph Tooby-Smith]

Looking at SICM in more detail, it looks like it would serve as a pretty good foundation for building further API around classical mechanics in PhysLean more generally (to serve purpose 1 as well as 2 in Nicola's message above), if that is something you would be interesting in helping contribute to.

[Alok Singh]

I was looking into this earlier in the year, but got caught up working on an array library and floats before this. But it’s still something I want to see.

[Rein Zustand]

Julia makes more sense than Clojure/Haskell IMO, given that it is also a Lisp under the hood (femtolisp), and is more tailored for numerical computation, which SICM is. Someone did this already: https://github.com/MasonProtter/Symbolics.jl (this person is a moderator of Julia Zulip community). I didn't follow this project, but it has since evolved into https://github.com/JuliaSymbolics/Symbolics.jl, but not sure.

[Mark Ettinger]

Interesting, Julia is indeed a reasonable choice. The original project looks dead and pretty incomplete. The second project looks more like SymPy than anything related to SICM. I may be interested in pursuing this in Lean but I also may try to get back to my formalization of special relativity which I paused when I got stuck some time ago.

[Rein Zustand]

The second project looks more like SymPy than anything related to SICM.

My memory is fuzzy (I took Sussman's class about SICM back in the day, together with the co-creator of Julia, Jeff Bezanson), but I think because scmutils can be used to solve the Lagrangian / Hamiltonian with / without constraints using CAS.

[Rein Zustand]

In the spirit of #PhysLean > Formalizing Landau and Lifshitz @ 💬 , we could also start with formalizing elegant reasonings in SICM. One example is that after deriving the Lagrangian mechanics, you define an entity H = (Legendre transform of Lagrangian). And then you apply the principle of stationary action, to $\int (p \dot{q} - H) dt$, you get $\dot{q}^a = \frac{\partial H}{\partial p_a}$ and $\dot{p}_a = - \frac{\partial H}{\partial q^a}$

[Mark Ettinger]

Regarding SICM, my personal interest favors project #2 over project #1, i.e. reproducing SICM in Lean for pedagogical purposes rather than formalization. However regarding formalization, I've made significant progress on one approach to special relativity which you can see here if so inclined: https://github.com/mettinger/Relativity.

[Joseph Tooby-Smith]

@Rein Zustand FYI, we already have this derivation of Hamilton's equations from the principle of Least action in PhysLean :) (see here, this is probably one of the files which needs documentation improved).

[Rein Zustand]

Would it be fine to add SICM as a reference in that HamiltonsEquations.lean file?

[Joseph Tooby-Smith]

Yeah! I think said reference would be great - the more specific the better (eg page number). Would be great if you could make a PR with this.

(I’m currently on a plane so may be a while before I personally have chance to respond to your other messages here)