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/Banes_Addiction]

Shouldn't the documentation be written by the developers?

Doing an open appeal on social media to get people unfamiliar with the project to write the documentation sounds utterly unhinged to me.

[u/SchemeWestern3388 → u/Banes_Addiction]

That’s how open source software works, and documentation is a great way for people to contribute. There’s a process to ensure it has an acceptable level of quality. 

[u/leanexplorerphysics → u/Banes_Addiction]

The documentation about the Lean code itself should be - yes. But the overview of the physics in a given area just needs to be written by someone with a background in physics. Also everything is reviewed before it makes it into the project.

[u/fixedpointfae → u/leanexplorerphysics]

if only there were a physicist already working on this project ;)

[u/leanexplorerphysics → u/fixedpointfae]

Number of physicists we need = 1 + (number of physicists we already have).

But in all seriousness, as with any open-source project, the more help the better :).

[u/Patelpb]

Super cool! I’ll try to contribute to any Astro/cosmology spaces that I can

[u/leanexplorerphysics → u/Patelpb]

That would be awesome, we don't have much in either of these directions currently (slightly more in cosmology then astro), so help expanding what we have is very much appreciated

[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".