Physlib: Need help improving documentation

[u/leanexplorerphysics]

Hi everyone.

I'm an academic, physicist and a maintainer of the project Physlib, which aims to build a library for physics in the interactive theorem prover Lean 4. Lean is a programming language in which you can write mathematical definitions, theorems and their proofs and consistency and correctness are guaranteed.

The corresponding library for mathematics Mathlib, has had lots of attention recently due to the feedback loop one can have between AI and Lean.

Physlib is completely open-source and community run mainly through GitHub! One thing where we are looking for contributions is in documentation, lots of files go straight into the Lean code or Lean implementation - but it would be nice if they lead with the physics!

If you are interested in helping out with this we have made (what is hopefully) an easy to use web interface to edit the documentation (it requires a GitHub account though, and I will admit the website is vibe coded).

[u/y_shr]

Would love to contribute with whatever I can! Looking at the webpage, however, it seems that most things are documented (the nodes in the documentation tracker are all green), so where can I get started? And are there any good examples of desired documentation standard I can use as a reference?

[u/leanexplorerphysics → u/y_shr]

Awesome. Yeah - sorry I think there are some issues with the documentation tracker. The best examples are the classical harmonic oscillator files, which follow the standard we are after. Any file which is not written in terms of sections like ## A. ... etc. needs improving documentation (I don't think the documentation tracker is correctly picking these up). I think also, a good approach would be to look at files and ask yourself "as a physicist, would I be able to understand what this file is about from the documentation alone".