Help with a <30 min task involving pendulums

Stream: PhysLean

[Joseph Tooby-Smith]

In part following on from #PhysLean > Formalizing Landau and Lifshitz .

Would someone volunteer to do the following?

1. Create a Pendulums directory in ClassicalMechanics within PhysLean.
2. For Problems 1, 2 and 3 of Section 5 of Landau and Lifshitz create an appropriately named file (adding the file to PhysLean.lean).
3. Add a documentation string at the top of the file with an overview of the problem, e.g. what the set-up is, what the Lagrangian is etc. Include a reference to L&L.
4. Make a PR with this.

[Shlok Vaibhav]

Is this task currently open and the same? (There seems to be no folder named Pendulum in ClassicalMechanics).
In case no one is working on this, I would like to do this.

[Joseph Tooby-Smith]

Hi Shlok, Yes, this is open and should be the same as I have written it above, so feel free to do this :). You will probably have to create the Pendulum directory.

[Shlok Vaibhav]

Is the following docstring fine for the first problem? (I assumed no lean code was expected, the description was meant as a comment in lean? :sweat_smile: is that right?).
The file name is LnL_V1_3E_Ch1_Sec5_P1_Coplanar_Double_Pendulum

/-
Source:
Textbook: Landau and Lifshitz, Mechanics, 3rd Edition
Chapter 1 The Equations of motion
Section 5 The Lagrangian for a system of particles
Problem 1: Coplanar Double Pendulum

Description: This problem involves:
a) identifying the appropriate Degrees of Freedom or generalized coordinates and their relation to cartesian coordinates
b) and using them to write down the Lagrangian for

a coplanar double pendulum made up of two point masses m1 and m2. m1 is attached to the
pivot and m2 is attached to m1 via strings of length l1 and l2 respectively.

Solution:
a) The cartesian coordinates (x1,y1) (For m1) and (x2,y2) (for m2) can be expressed with the
two angles made by the strings with vertical φ1 and φ2 and two constraints on distance between m1 and pivot and m2 and m1.
b) The Lagrangian is obtained by writing down the kinetic and potential energies first in terms of cartesian coordinates
and their time derivates and then substituting the coordinates and derivatives with transformations obtained in a)

-/

image.png

[Joseph Tooby-Smith]

I think including some of the equations would be worth while. I.e. I think someone should be able to formalize this without necessarily needing to open L&L. But yeah, no Lean code :).

[Joseph Tooby-Smith]

Also I would rename it to something like CoplanerDoublePendulum.lean, taking the focus of L&L and on the problem it corresponds to (if that makes sense).

[Shlok Vaibhav]

Joseph Tooby-Smith said:

I think including some of the equations would be worth while. I.e. I think someone should be able to formalize this without necessarily needing to open L&L. But yeah, no Lean code :).

Okk got it, that makes sense, aim is for people to take this file as a formalization exercise and not a classical mechanics course and a good docstring should preclude opening L&L. Will send the changes tomorrow.

I will make the name change as well (I thought having identifiers in name will make it easier to sort and search and document the progress on each book but this makes the name more like an insurance policy number and the identifiers like book, edition and chapters can be parsed from the docstring equally well)

[Joseph Tooby-Smith]

(I thought having identifiers in name will make it easier to sort and search and document the progress on each book but this makes the name more like an insurance policy number and the identifiers like book, edition and chapters can be parsed from the docstring equally well)

We could also make attributes that are connected to specific books, e.g. @[L&L 1.5.1]... maybe making something like this for arxiv papers would also be good.

[Shlok Vaibhav]

How's the following docstring? (Vscode could do most of the autofill when prompted correctly)

/-   {LnL_1.5.1}
Source:
Textbook: Landau and Lifshitz, Mechanics, 3rd Edition
Chapter 1 The Equations of motion
Section 5 The Lagrangian for a system of particles
Problem 1: Coplanar Double Pendulum

Description: This problem involves:
a) identifying the appropriate Degrees of Freedom or generalized coordinates and their relation to cartesian coordinates
b) and using them to write down the Lagrangian for

a coplanar double pendulum made up of two point masses m1 and m2. m1 is attached to the
pivot and m2 is attached to m1 via strings of length l1 and l2 respectively.

Solution:
a) The cartesian coordinates (x1,y1) (For m1) and (x2,y2) (for m2) can be expressed with the
two angles made by the strings with vertical φ1 and φ2 and two constraints on distance between m1 and pivot and m2 and m1:
x1 = l1 sin(φ1)
y1 = - l1 cos(φ1)
x2 = l1 sin(φ1) + l2 sin(φ2)
y2 = - l1 cos(φ1) - l2 cos(φ2)

b) The Lagrangian is obtained by writing down the kinetic and potential energies first in terms of cartesian coordinates
and their time derivates and then substituting the coordinates and derivatives with transformations obtained in a):

L = T1 + T2 - V1 - V2 where
T1 = 1/2 m1 (x1_dot^2 + y1_dot^2) = 1/2 m1 l1^2 φ1_dot^2  (Kinetic energy of m1)
V1 = m1 g y1 = - m1 g l1 cos(φ1)                          (Potential energy of m1)
T2 = 1/2 m2 (x2_dot^2 + y2_dot^2) = 1/2 m2 [l1^2 φ1_dot^2 + l2^2 φ2_dot^2 + 2 l1 l2 φ1_dot φ2_dot cos(φ1 - φ2)] (Kinetic energy of m2)
V2 = m2 g y2 = - m2 g [l1 cos(φ1) + l2 cos(φ2)]                     (Potential energy of m2)

so that the Lagrangian becomes:
L = 1/2 (m1 + m2) l1^2 φ1_dot^2 + 1/2 m2 l2^2 φ2_dot^2 + m2 l1 l2 φ1_dot φ2_dot cos(φ1 - φ2)
    + (m1 + m2) g l1 cos(φ1) + m2 g l2 cos(φ2)
-/

[Joseph Tooby-Smith]

This looks along the right lines to me!

[Shlok Vaibhav]

I've raised a pull request for the three problems, however, I am getting a spurious minus sign in part c of the third problem which is absent from textbook solution, can someone check my solution?
20251124_232034.jpg
The red part in textbook solution is where I am getting an extra minus (The last term in last line of my solution)
image.png

[ZhiKai Pong]

The book has positive y downwards, I think it's just this

[Shlok Vaibhav]

That would flip the sign of the potential term m g l cos(phi) as well?

[Shlok Vaibhav]

image.png
Can someone help with this lean based style linter check failing for pull request? I wasn't seeing this yesterday.

[Joseph Tooby-Smith]

You need to update the ‎PhysLean.lean‎ to reflect the new names of the modules :) - it still uses the underscored names

[Shlok Vaibhav]

Ohh sorry, i updated file names but forgot to do the same in PhysLean.lean

[Joseph Tooby-Smith]

Shlok Vaibhav said:

That would flip the sign of the potential term m g l cos(phi) as well?

I think what Zhi-Kai is saying is that $y=-a \cos \gamma t - l \cos \phi$.
(Alternatively, if you replace $a$ with $-a$ in your solution, then you will get the right result).

[Shlok Vaibhav]

Ahh got it, flipping sign of "a" works, thanks!

[Joseph Tooby-Smith]

The PR looks great Shlok! Many thanks for doing this - it is very much appreciated . Hopefully it wasn't too painful, and will act as an impetus for more contributions like this.

[Shlok Vaibhav]

So here if i think in terms of the initial conditions, in either case

$$y(0) = \pm a \quad ( \text{Let } \phi(0)=0)$$

So writing my lagrangian in terms of the initial condition would give in both cases:

$$L = (...)+(...) - m\gamma^2ly(0)\cos \gamma t \cos \phi$$

doing away with the sign ambiguity

[Shlok Vaibhav]

Is this correct?

[Joseph Tooby-Smith]

I think this would be a dangerous way to write the Lagrangian. The Lagrangian should be defined for all trajectories (even those that don't satisfy the equations of motion), so you can't choose $\phi(0) = 0$.
The Lagrangian you have written down is would have a different set of equations of motion, and is fairly complicated, because it is non-local.

Another way to put this, you shouldn't be talking about initial conditions at the stage of writing down the Lagrangian.

[ZhiKai Pong]

does https://physlean.com/docs/ not automatically update? I'm trying to see how it looks on there, just thinking about whether it'll be nicer if the equations are in latex.

[Joseph Tooby-Smith]

The docs update twice a day, and I think the last update was before this was merged, so might have to wait until tonight, or generate them locally. But I think latex would be nice here

[Shlok Vaibhav]

You mean keeping latex code in docstring within $$ will render equations on docs page? Is there such an arrangement?

[ZhiKai Pong]

yea, see e.g. here (with source)

might need some tinkering though, I found this from this thread #mathlib4 > LaTeX in docstrings which suggests there are some issues with displaying them properly

[Shlok Vaibhav]

Thanks for sharing, I will try this soon on these docstrings

[ZhiKai Pong]

Btw I think the docstrings should start with /-!, currently it still doesn't show up in the docs

[Joseph Tooby-Smith]

Hmm, this is making me a bit worried, that one of the linters isn't working properly on these files, as these sorts of things should have been pulled up by the ./scripts/lint-style.sh linter. I wonder if it is because they have no Lean content.

[Shlok Vaibhav]

Okk then maybe I can commit the files again with bare minimum lean content like just the import statements? It will then do all checks correctly?

[Joseph Tooby-Smith]

Yeah, mabye we could just put an import PhysLean.SpaceTime.Space.Basic at the top of each file, and see what happens in terms of the linters - would be a good check.

[Shlok Vaibhav]

Okk so I will do this now, let's see in an hour

[Shlok Vaibhav]

So in one of the files, I made the equation portion of comment start with /-! as well as added the import statement before this comment section (I hope this is the minimally correct version?) and in one of the files, just the import statement, there are no errors during the linter checks in a draft pr i made for this change.

[Shlok Vaibhav]

Also, I need to visualize how the latex code in the comment shows up in html before I can made the new PR. As per the link shared by ZhiKai, i should be using https://github.com/leanprover/doc-gen4 on my machine, is this right?

[Joseph Tooby-Smith]

Shlok Vaibhav said:

Also, I need to visualize how the latex code in the comment shows up in html before I can made the new PR. As per the link shared by ZhiKai, i should be using https://github.com/leanprover/doc-gen4 on my machine, is this right?

I think running lake build PhysLean:docs should do it, no need to install anything, docgen4 is already imported into PhysLean.

[Joseph Tooby-Smith]

Ok, I did some digging:

The copyright check and the check of the module doc-string happen in this line:

https://github.com/HEPLean/PhysLean/blob/ae0a4f17d7239f8d8a7da8da92ee2aa969e56878/scripts/lint-style.py#L439

Which is not checked by files which are "import"-only. A work around is to add:

namespace ClassicalMechanics

end ClassicalMechanics

to each of these files. But I think in the end we should improve or update this linter (not least because it weirdly depends on commits to github, which I find annoying).

[Shlok Vaibhav]

This works, now its flagging docstring's absence.

[Shlok Vaibhav]

image.png
I've created docstring for one problem as shown in the image, looking for suggestions on this (Will implement for other two files as well) here's the code (you can edit this to emphasize the changes needed):

/-
Copyright (c) 2025 Shlok Vaibhav Singh. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shlok Vaibhav Singh
-/
/-!
# Sliding Pendulum
### Tag: LnL_1.5.2
## Source
* Textbook: Landau and Lifshitz, Mechanics, 3rd Edition
* Chapter: 1 The Equations of motion
* Section: 5 The Lagrangian for a system of particles
* Problem 2: Sliding Pendulum

## Description
A simple pendulum of mass $m_2$ attached to a mass $m_1$ as its point of support via a string of length $l$.
The mass $m_1$ is free to move horizontally. The lagrangian of the system is to be found.

## Solution
First, the constraints are identified:
$$
\begin{align}
y_1 &= 0 \\
(x_2 - x_1)^2 + (y_2-y_1)^2 &= l^2
\end{align}
$$
So that $x_2-x_1 = l \sin(\phi)$ and $y_2-y_1 = y_2 = - l \cos(φ)$ with the generalized coordinate, $φ$,
being the angle the string makes with vertical.

The Lagrangian is obtained as:
$$\mathscr{L} = T_1 + T_2 - V_1 - V_2$$ where
* Kinetic energy of $m_1$   :    $\quad T_1 = \frac{1}{2} m_1 \dot{x}_1^2 $
* Potential energy of $m_1$:     $\enspace V_1 = 0$
* Kinetic energy of $m_2$  :     $\quad T_2 = \frac{1}{2} m_2 (\dot{x}_2^2 + \dot{y}_2^2) = \frac{1}{2} m_2 [l^2 \dot{φ}^2 + \dot{x}_1^2 + 2 l \dot{φ} \dot{x}_1 \cos(φ)]$
* Potential energy of $m_2$:     $\enspace V_2 = m_2 g y_2 = - m_2 g l \cos(φ)$

So that
$$\mathscr{L} = \frac{1}{2} (m_1 + m_2) \dot{x}_1^2 + \frac{1}{2} m_2 (l^2 \dot{φ}^2 + 2 l \dot{φ} \dot{x}_1 \cos(φ)) + m_2 g l \cos(φ)$$

-/

namespace ClassicalMechanics

end ClassicalMechanics

[Joseph Tooby-Smith]

This looks very nice @Shlok Vaibhav :).

[Joseph Tooby-Smith]

@Shlok Vaibhav out of interest, how did you go about viewing the docs locally? Did you just open the specific html file? I'm wondering if there is a specific, more fancy way.

[Joseph Tooby-Smith]

For each of these pendulums i think the next step is to define the data-structure which contains their configuration spaces, and build an API around these. For example, the configuration space for the sliding pendulum is likely the following:

structure ConfigurationSpace (l : ℝ) where
  y1 : ℝ
  y2 : ℝ
  x1 : ℝ
  x2 : ℝ
  y1_zero : y1 = 0
  pendulum_length_eq : (x2 - x1) ^ 2 + (y2-y1) ^ 2 = l ^ 2

which then would probably want to endow with the instance of a manifold, but there are lots of little other lemmas one could show as well.

[Shlok Vaibhav]

So I first tried to build only the specific file by executing "lake build PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum:docs" but this generates very incomplete html
image.png
So i executed "lake build PhysLean:docs" to get the actual page rendering. After that i just kept rebuilding the specific file (fast, <10 seconds) and viewing the html in .lake folder in my browser, did i understand the query correctly?

[Shlok Vaibhav]

Also, have raised a pull request with these comments updated for the three files

[Joseph Tooby-Smith]

Shlok Vaibhav said:

So I first tried to build only the specific file by executing "lake build PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum:docs" but this generates very incomplete html
image.png
So i executed "lake build PhysLean:docs" to get the actual page rendering. After that i just kept rebuilding the specific file (fast, <10 seconds) and viewing the html in .lake folder in my browser, did i understand the query correctly?

Yep, this makes sense, and answers my question! Many thanks.

[Joseph Tooby-Smith]

Shlok Vaibhav said:

Also, have raised a pull request with these comments updated for the three files

Great, these pages look really good! I've approved and merged your PR.

[Joseph Tooby-Smith]

It would be a huge amount of work, but I think one day we should definitely be aiming for all of our documentation to look as good as these examples.

[Shlok Vaibhav]

Joseph Tooby-Smith said:

It would be a huge amount of work, but I think one day we should definitely be aiming for all of our documentation to look as good as these examples.

The pipeline looked as follows:

1. Deriving equations by hand
2. Typing these equations and one-line explanations in lean comment in very informal manner (using x_dot for time derivative) - The github copilot is quite smart here and can actually autocomplete a significant (~50%) fraction of the lines, though still misses context of equations a lot.
3. Converting one file manually into correct latex-format equations and then asking copilot to convert other files from informal maths to latex-format and it can do this step quite correctly, i didn't notice any sign mistake or missed variable. And it can decipher from the fed example certain rules, like any L for lagrangian has to be written as \mathcal{L} and not just L or that I prefer sin(phi) instead of sin phi

3 needs a suitable prompting like telling the comment line length shouldn't exceed 100 and any new line shouldn't start with +,-,* etc. 3 also requires comparison of equations with the handwritten ones to still check for any inadvertant errors.

[Shlok Vaibhav]

As such, most time-taking activity was 1 with 2 and 3 more like review tasks, not taking more than 10-15 mins each, so fortunately solving the problem by hand is both the best and the heaviest part, rest two steps being mainly managerial supervision

[Shlok Vaibhav]

Joseph Tooby-Smith said:

For each of these pendulums i think the next step is to define the data-structure which contains their configuration spaces, and build an API around these. For example, the configuration space for the sliding pendulum is likely the following:

structure ConfigurationSpace (l : ℝ) where
  y1 : ℝ
  y2 : ℝ
  x1 : ℝ
  x2 : ℝ
  y1_zero : y1 = 0
  pendulum_length_eq : (x2 - x1) ^ 2 + (y2-y1) ^ 2 = l ^ 2

which then would probably want to endow with the instance of a manifold, but there are lots of little other lemmas one could show as well.

can you point to other files that have such problems or flow attempted? As per my understanding, set of noncomputable defintions are going to be:

1. L = T-V
2. T = 1/2m(x^2+y^2)
3. V = mgy
   Along with the two hypothesis in the structure you defined, the task is to prove L(x,y) = L(phi) with the coordinate transformation shown to be proper as well. Is this correct
   Is this correct?

[Joseph Tooby-Smith]

c.f. your first message Shlok, this pipline is good to know! In the cases where we already have things formalized, and it is a case of just writing proper documentation, then I think (1) should be much easier, since the problem is actually already solved. But for new files, I agree that (1) is probably the most difficult here :).

[Joseph Tooby-Smith]

Shlok Vaibhav said:

can you point to other files that have such problems or flow attempted? As per my understanding, set of noncomputable defintions are going to be:

1. L = T-V
2. T = 1/2m(x^2+y^2)
3. V = mgy
   Along with the two hypothesis in the structure you defined, the task is to prove L(x,y) = L(phi) with the coordinate transformation shown to be proper as well. Is this correct
   Is this correct?

The closest thing we have to this is the harmonic oscillator example, however, this currently doesn't use a configuration space, which it probably should - will require a refactoring. I think your definitions are the main ones, but there are probably some other ones like:

1. Spatial point of the first particle ConfigurationSpace l → Space 2.
2. Spatial point of the second particle ConfigurationSpace l → Space 2.
3. The angle φ.
4. Probably worth defining T1, T2, V1 and V2 separately as well.

[Joseph Tooby-Smith]

Along with the two hypothesis in the structure you defined, the task is to prove L(x,y) = L(phi) with the coordinate transformation shown to be proper as well. Is this correct

Sorry, got distracted mid way from responding. Yes, essentially I think the task would be to write down the Lagrangian, and write it in different forms. If we could go further from their and derive the equations of motion, I think that would be great, but probably not worth worrying about right now.

[Shlok Vaibhav]

I was going through (somewhat incomplete) paper on augmenting LLMs with Lean4 based formalized high school physics problems : https://arxiv.org/html/2510.26094v1 . I found this one para relevant to what we are trying here (NL: Natural language, used in textbook):
image.png
What is suggested is to use LLM to generate a theorem from the problem to supplied and this can be then fed to a physlean augmented LLM. So the first step here: generating a theorem from natural language is something that can be relevant in formalizing textbooks? (After reading this paper, i asked gemini to solve a problem on pendulum from landau lifshitz and it couldn't reduce it satisfactorily but it thought about using integration by parts to obtain total time derivatives and then drop it, maybe their approach may work for lighter texts but not for more rigorous or graduate level texts?)

[Joseph Tooby-Smith]

generating a theorem from natural language is something that can be relevant in formalizing textbooks?

I think if we can find an AI that would reliably do this "autoformalization", it would be great, in particular, it could be applied to the "informal lemmas" and "informal definitions" in Lean. (If I haven't missed the point here). FYI, there are some dicussions on this paper here.

[Shlok Vaibhav]

Thanks for pointing out! missed the thread somehow