PhysLean
@physlean.bsky.social
A project to digitalize physics into the interactive theorem prover lean 4.
Account for news related to the project. Run by: Joseph Tooby-Smith.
Account for news related to the project. Run by: Joseph Tooby-Smith.
There is lots of potential for follow up results, including, naturally the 3d version, and generalizations to planes and lines of charges. See the project here:
July 23, 2025 at 2:10 PM
There is lots of potential for follow up results, including, naturally the 3d version, and generalizations to planes and lines of charges. See the project here:
Since the charge density of a point particle is a dirac delta function, the proof of this result requires use of distributions, and thus creating an API for distributions that aligns with the physicists needs and approaches, which has been done!
July 23, 2025 at 2:10 PM
Since the charge density of a point particle is a dirac delta function, the proof of this result requires use of distributions, and thus creating an API for distributions that aligns with the physicists needs and approaches, which has been done!