Formalizing Landau and Lifshitz

Stream: PhysLean

[Joseph Tooby-Smith]

I met with @ZhiKai Pong last Thursday, and one of the things that suggested again was to create a project to try and pick a book e.g. the Feynman lectures or Landau and Lifshitz and try and go through and formalize it into PhysLean.

This is something we discussed briefly at the last PhysLean Cafe. And I think, @Afiq Hatta was mentioning something in this direction.

I think one could make the make things more definite by e.g. restricting to certain parts of the book, for example, the goal could be:

Formalize every physical classical mechanics system mentioned in Landau and Lifshitz vol 1.

Naturally doing something along this lines, will force us to also formalize the necessary API.

Would there be a general interest to 1) help think about the organization and structure of such a project within PhysLean, and/or 2) help directly with the formalization?

[Matteo Cipollina]

Joseph Tooby-Smith ha scritto:

Would there be a general interest to 1) help think about the organization and structure of such a project within PhysLean, and/or 2) help directly with the formalization?

I'm in for 1) and 2) on L&L, improving on our (partial) attempts to ground our formalization in the Statistical Mechanics folder on L&L.

[Joseph Tooby-Smith]

Let me add when it is on my mind, I think one thing we should be careful of in undertaking this sort of project, is that it should not come at the sacrifice of good, general API that fits the subject (which is what we want for PhysLean) not the book, if this makes sense. I'm not sure how big a danger this is, or even if it is possible, but I thought I would write it down anyway.

[Daniel Morrison]

I've thought about doing something like this to get a whole list of related concepts, but my concern is how to get started. I think we'll run into the problem that the book makes assumptions that we don't want to make in PhysLean. Maybe it's a matter of finding the rights texts to use.

[Joseph Tooby-Smith]

Maybe one option of how to start would be to state things at a really high level, e.g. from the point of view of PhysLean, the modules (files) one would need to make, or even just the directories.

[Joseph Tooby-Smith]

I think there are three things to think about here:

1. What is the best book?
2. Do we need any infrastructure to help with this, and if so what? (I think @Afiq Hatta might have something that helps in the pipeline). In addition maybe something like a google-doc to list books or parts of books etc.
3. What is the workflow to take the content into PhysLean?

[Afiq Hatta]

I think in terms of mechanics texts there are a few options, but I vote
landau. I've listed the famous texts below. I'm working on a tool this
weekend that helps me annotate texts! But for rough structure, I think a
google doc works best that we can all easily collaborate on. In terms of
workflow, informal lemmas were easy enough to start with.

Morin Taylor Goldstein Landau Lif VI Arnold

[Joseph Tooby-Smith]

Maybe a google sheet like the following (very quickly put together and not suggesting this is the 'final' thing, just an idea):

https://docs.google.com/spreadsheets/d/1pGaVqod1XtBfNTejdlN73PfHvl_xUeuKjS4tjBp4f6g/edit?usp=sharing

As long as the results follow each other in the right order, I don't think we actually need to restrict ourselves to one book, although maybe down this road leads chaos.

[Joseph Tooby-Smith]

(In case the link doesn't work, which it doesn't seem to for me :()

Screenshot 2025-10-31 at 16.38.15.png

[Afiq Hatta]

works for me - i'll fill in this tonight with more results to check if it feels natural

[Daniel Morrison]

I'd suggest maybe listing sections or chapters or page numbers leading to a certain result otherwise I can see the spreadsheet becoming quite long. Also I think it would be nicer to claim a collection of related statements rather than one at a time. I'm more familiar with the math side of things so I'm not too familiar with the best texts to follow for physics and this would be helpful for me personally.

[Joseph Tooby-Smith]

Maybe there is a way to organize the google sheet where we could have layers of details. A layer for chapters or collections of results (i.e. bigger level topics) and layers with more fine-grained details.

[Joseph Tooby-Smith]

I made some improvements, here is a link I think people may be able to use to edit. I tried to allow people to claim a add of results with the 'directory' option. Anyone should feel free to edit/improve:

https://docs.google.com/spreadsheets/d/1pGaVqod1XtBfNTejdlN73PfHvl_xUeuKjS4tjBp4f6g/edit?usp=sharing

[Joseph Tooby-Smith]

I wonder if a similar google doc thing would work for suggestions to improvements for documentation. I made https://physlean.com/DocumentationTracker, which tracks which documentation needs improving. But it would be nice if people could just edit a google doc to contribute. I'm less sure what this would look like.

[Joseph Tooby-Smith]

Joseph Tooby-Smith said:

I wonder if a similar google doc thing would work for suggestions to improvements for documentation. I made https://physlean.com/DocumentationTracker, which tracks which documentation needs improving. But it would be nice if people could just edit a google doc to contribute. I'm less sure what this would look like.

Something along these lines:
https://docs.google.com/document/d/1fEyqrCTqYyTL6WRGSw5nw8QU3h8-TLKGKBnuvaJ12Xk/edit?usp=sharing

[Rein Zustand]

We could start with cherry-picking some of the most elegant derivations from Landau. E.g. this is an argument why the Lagrangian of a free particle has to be in the form of $\propto v^2$

The argument proceeds from fundamental symmetry principles:

1. Homogeneity of space: L cannot depend on position
2. Homogeneity of time: L cannot depend explicitly on time
3. Isotropy of space: L can only depend on |v|² (not direction)
4. Galilean invariance: Physics must be the same in all inertial frames

From these principles, we derive that the only consistent form for the free particle
Lagrangian is L = (const) · v² = ½mv².

[Rein Zustand]

Sorry, that's Claude Code being incomplete in including the argument. There should be a total time derivative gauge equivalence that eventually result with any variation being equivalent to just $Cv^2$.

[Joseph Tooby-Smith]

I think the inclusion of a proof along these lines would be very nice. Again we would want it to fit with the rest of the API, but that should be easy enough in this example

[Rein Zustand]

Yeah, I'm currently stuck with the EPR one because it has too many dependencies not being built yet. Currently attempting the Landau free particle instead.

[Rein Zustand]

https://github.com/HEPLean/PhysLean/pull/849 accidentally opened this as ready-for-review. This costed me about ~$11 of Claude Opus 4.5 haha, with rounds of bug fixes and clarifications of the informal reasonings.

[Joseph Tooby-Smith]

So I think this PR falls into my earlier worry about integration with API.

There are lots of things in it, e.g. boosts and Galilean invariance, which should be part of the general API (and in some cases are), and not defined for this specific problem. Building APIs prevents us having the same results repeated in lots of different places, and makes the whole problem easier to navigate and use.

I think this is one of the places where AI currently struggles.

[Rein Zustand]

I see. At least it is a good starting point! I initially thought the derivation/formalization in that PR would be deemed unnecessarily complicated. I can fix this.

[Rein Zustand]

1. Should I put the Galilean group/boost in the Relativity folder, or in ClassicalMechanics folder?
2. CC struggled with implementing a general Galilean transform. Is it fine if it just does Galilean boost for now? If not, I'm fine with no cutting corners, and figure out a way.

[Rein Zustand]

Also, please do say if reviewing an AI slop would waste your valuable time; if I am being inconsiderate. Zulip contributing guide has a section for it actually: https://github.com/zulip/zulip/blob/17ea45a392b14795b15a4ab9f6132518cf4f0b03/CONTRIBUTING.md?plain=1#L38-L39C25.

[Joseph Tooby-Smith]

Yep - good starting point for ideas :).

For the Galilean group, I think it should be in this directory:

https://github.com/HEPLean/PhysLean/tree/master/PhysLean/SpaceAndTime/TimeAndSpace

since it is a group acting on Time x Space in the non-relativistic setting.

1. CC struggled with implementing a general Galilean transform. Is it fine if it just does Galilean boost for now? If not, I'm fine with no cutting corners, and figure out a way.

Yes, this is fine (under the philosophy that something is better than nothing). But it is better to implement the full Galilean group, or at the very least write a TODO item about it.

Also, please do say if reviewing an AI slop would waste your valuable time; if I am being inconsiderate.

It is a waste of my time if I'm the first person to look through it and ask how it fits within the project, if it makes sense, etc. Because in that situation I may as well have just done it myself. (Making a general statement here, and not claiming this is the case here).

From the point of view of reviewing, the thing that makes it as easy as possible is to split PRs into as small chunks as possible (even individual lemmas or documentation etc. - at least initially). In these cases, the road from making a PR to it being merged is often much shorter (which I think benefits everyone). This is something which is also said about Mathlib.

[Joseph Tooby-Smith]

Concerning the Galilean group, I have made this GitHub issue PhysLean#911, which specifies the structure of the API and requirements. I think this would be a nice little project to build up these requirements for anyone wanting to get their hands dirty building APIs for PhysLean.