@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.
A YouTube short on Lean & PhysLean:
www.youtube.com/shorts/BdZ44...
New independent paper out utilising PhysLean :)
arxiv.org/pdf/2601.030...
Part of PhysLean is about building good APIs around #physics concepts in #LeanLang. To this end, we have made the following GitHub project to track progress in this direction:
github.com/orgs/HEPLean...
For further info see the PhysLean Zulip channel:
leanprover.zulipchat.com#narrow/chann...
A chance to share your views on what PhysLean should look like and what should be done in 2026:
leanprover.zulipchat.com#narrow/chann...
#LeanLang #Physics
A short blog post about data structures, physics and Lean:
josephtoobysmith.com/cs/2025/12/1...
A video on downloading and installing Lean and PhysLean (without admin privileges):
www.youtube.com/watch?v=Uvte...
#LeanLang #Physics
PhysLean recently passed 400 stars on GitHub 😀
🔗 github.com/HEPLean/Phys...
#LeanLang #Physics #GitHub
AI summary of PhysLean monthly updates:
Key advancements include implementing Distribution Theory in Electromagnetism, a major refactor making Space a Structure, and proving lemmas for the FLRW cosmological metric. Content covers ideal gas and Landau & Lifshitz problems.
"A Perspective on Interactive Theorem Provers in Physics"
advanced.onlinelibrary.wiley.com/doi/10.1002/...
#physics #LeanLang
An AI summary of PhysLean's commits from this month:
added norm props, time/space integrals & radial angular measure; EM improvements (potentials, constants, plane waves); Lorentz action on distributions; FLRW cosmology formalization; plus refactors, linting & docs.
Recently added to the PhysLean website is a new tracking graph for documentation and instructions on how you can help contribute! See the link below:
physlean.com/Documentatio...
#physics #LeanLang
A talk on PhysLean for physics undergraduates can be found here:
www.youtube.com/watch?v=qcTf...
Part of a practice for a talk to be given tomorrow.
Yesterday we posted a graph for the formalization of Wick's theorem, today I made a little web-applet that allows you to explore interconnected files in PhysLean:
🔗 josephtoobysmith.com/Slides/PhysL...
As a specific example:
josephtoobysmith.com/Slides/PhysL...
Have been having fun making some graphs related to PhysLean! Here is one for the proof of Wick's theorem, which is the precursor to Feynman diagrams
(discussed in arXiv:2505.07939)!
Graph made using:
github.com/leanprover-c...
Here are some slides on PhysLean for a talk given at the EuroProofNet Workshop on Proof Libraries:
josephtoobysmith.com/Slides/Orsay...
#physics #LeanLang
If you are interested in helping PhysLean with it's documentation take a look at this message on the Lean Zulip:
leanprover.zulipchat.com#narrow/chann...
Can you help PhysLean make better documentation for the classical harmonic oscillator? If so take a look at this link where you can review what we currently have and make suggestions for improvements!
🔗 github.com/HEPLean/Phys...
Tutorial on how to contribute to PhysLean through golfing proofs🏌 :
📽️ www.youtube.com/watch?v=QL-m...
This is a good way to get involved if you are new to Lean but want to get stuck in.
#physics #LeanLang
If you want to follow what happens on PhysLean, the best way is to "watch" the project, and set the notification level to custom -> Pull Requests.
This way you will get notifications of new things being added to the project, and maybe you can spot something you are interested in or comment on.
Tutorial on how to add informal results to PhysLean - to do this you need know Lean background, just a knowledge of some areas of physics, and it is incredible helpful!
www.youtube.com/watch?v=f9kJ...
#physics #LeanLang
Diagram showing the digitalized physics in PhysLean!
Not perfect by any means, but hopefully is descriptive enough.
#physics #maths
(Delayed) summary of this (/last) week in PhysLean:
Discussions on Zulip about documentation and on-boarding. Improvements the issue tracker around bumps. Better API for Time, and properties of tanh for QM.
#physics #LeanLang
Summary of this week in PhysLean:
API improvments for finite-dimensional quantum systems, and charges in F-theory.
Creation and annihilation in the reflectionless potential in QM
Fundamental theorem of variational calculus proof.
Zulip proposal for forming teams with roles.
Four more projects added to the PhysLean ideas website:
physlean.com/ProjectIdeas
⭐️ Planck’s theory of blackbody radiation
💧 Hydrodynamic drag
🌊 Boltzmann equation
⚡️ Larmor formula
PhysLean news this week, in summary:
✅ Progress made on the units API following a conversation on the Zulip.
✅ The first steps have been made towards the reflectionless potential in quantum mechanics.
✅ New results related to the exponential map of the Lorentz group.
#physics #LeanLang
New video on the definition of 'time' in PhysLean:
www.youtube.com/watch?v=GnTQ...
#physics
News from PhysLean this week:
In short: we had a properties of the electric field of a 1d charged particle in relation to improvements to distributions, improvements to the 1d classical harmonic oscillator, and properties of the Lorentz algebra.
#LeanLang #Physics
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:
23.07.2025 14:10 — 👍 1 🔁 0 💬 1 📌 0Since 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!
23.07.2025 14:10 — 👍 1 🔁 0 💬 1 📌 0
