Classical Mechanics of a pendulum

Stream: PhysLean

[Trevor Huang]

Hi, I am a high school senior who is interested in plasma physics and randomly stumbled across this project. I am new to Lean, but I am eager to learn and willing to give the formalization of a pendulum task a serious attempt.

Any help/guidance would be greatly appreciated. It's nice to meet everyone!

[Scott Carnahan]

The full solution may require elliptic integrals (which we don’t seem to have yet) but the small-angle approximation sounds like a good place to start.

[Joseph Tooby-Smith]

Hi @Trevor Huang :wave:, nice to see you here!

I think the first step to take is to plan the area informally. There is a tutorial here:

https://www.youtube.com/watch?v=f9kJyQs92TM&list=PLQveF4ZJyPHrpTiKN8jbrJKfxDPBq49Hw&index=2

about how one can do this. I would recommend starting with really small pull-requests to the project (i.e. really small changes), as this makes it easier for us and also hopefully keeps things more motivating for you :). If you have any questions feel free to put them here.

[Tyler Josephson ⚛️]

Welcome!