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.
"A Perspective on Interactive Theorem Provers in Physics"
advanced.onlinelibrary.wiley.com/doi/10.1002/...
#physics #LeanLang
advanced.onlinelibrary.wiley.com/doi/10.1002/...
#physics #LeanLang
November 23, 2025 at 12:25 PM
"A Perspective on Interactive Theorem Provers in Physics"
advanced.onlinelibrary.wiley.com/doi/10.1002/...
#physics #LeanLang
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.
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.
November 12, 2025 at 9:49 AM
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.
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
physlean.com/Documentatio...
#physics #LeanLang
PhysLean: Digitalizing Physics in Lean 4
A project to digitalize results from physics into Lean 4.
physlean.com
November 1, 2025 at 10:49 AM
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
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.
www.youtube.com/watch?v=qcTf...
Part of a practice for a talk to be given tomorrow.
PhysLean: A talk for physics undergraduates
YouTube video by Joseph Tooby-Smith
www.youtube.com
October 22, 2025 at 9:51 AM
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.
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...
🔗 josephtoobysmith.com/Slides/PhysL...
As a specific example:
josephtoobysmith.com/Slides/PhysL...
PhysLean
josephtoobysmith.com
October 7, 2025 at 8:00 AM
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...
🔗 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...
(discussed in arXiv:2505.07939)!
Graph made using:
github.com/leanprover-c...
October 6, 2025 at 9:06 AM
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...
(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
josephtoobysmith.com/Slides/Orsay...
#physics #LeanLang
PhysLean
josephtoobysmith.com
October 2, 2025 at 10:38 AM
Here are some slides on PhysLean for a talk given at the EuroProofNet Workshop on Proof Libraries:
josephtoobysmith.com/Slides/Orsay...
#physics #LeanLang
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...
leanprover.zulipchat.com#narrow/chann...
Public view of Lean | Zulip team chat
Browse the publicly accessible channels in Lean without logging in.
leanprover.zulipchat.com
September 17, 2025 at 4:13 PM
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...
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...
🔗 github.com/HEPLean/Phys...
September 12, 2025 at 3:07 PM
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...
🔗 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
📽️ 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
Tutorial: Golfing proofs in PhysLean
YouTube video by Joseph Tooby-Smith
www.youtube.com
September 8, 2025 at 7:14 AM
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
📽️ 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.
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.
September 2, 2025 at 8:57 AM
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.
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
www.youtube.com/watch?v=f9kJ...
#physics #LeanLang
Tutorial: Adding Informal Results to PhysLean
YouTube video by Joseph Tooby-Smith
www.youtube.com
August 29, 2025 at 7:56 AM
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
www.youtube.com/watch?v=f9kJ...
#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.
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.
August 9, 2025 at 9:14 AM
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.
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.com/ProjectIdeas
⭐️ Planck’s theory of blackbody radiation
💧 Hydrodynamic drag
🌊 Boltzmann equation
⚡️ Larmor formula
Project ideas
A project to digitalize results from physics into Lean 4.
physlean.com
August 4, 2025 at 9:31 AM
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.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
✅ 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
August 1, 2025 at 5:07 PM
Defining time in PhysLean
YouTube video by Joseph Tooby-Smith
www.youtube.com
July 28, 2025 at 4:17 PM
A charged point particle in 1 dimension generates a constant electric field in each direction pointing away (or towards depending on the charge) from it. Physically this makes sense, since there is nowhere for the 'electric flux' to spread out.
We now have a proof of this in PhysLean!
We now have a proof of this in PhysLean!
July 23, 2025 at 2:10 PM
A charged point particle in 1 dimension generates a constant electric field in each direction pointing away (or towards depending on the charge) from it. Physically this makes sense, since there is nowhere for the 'electric flux' to spread out.
We now have a proof of this in PhysLean!
We now have a proof of this in PhysLean!
The PhysLean website now contains a 'project ideas' page, if you want to get involved in the project but don't know what to do:
🔗 physlean.com/ProjectIdeas
If you are a physicists and have any ideas of what you would like formalizing, would love to hear them!
#physics #science
🔗 physlean.com/ProjectIdeas
If you are a physicists and have any ideas of what you would like formalizing, would love to hear them!
#physics #science
Project ideas
A project to digitalize results from physics into Lean 4.
physlean.com
July 17, 2025 at 3:44 PM
The PhysLean website now contains a 'project ideas' page, if you want to get involved in the project but don't know what to do:
🔗 physlean.com/ProjectIdeas
If you are a physicists and have any ideas of what you would like formalizing, would love to hear them!
#physics #science
🔗 physlean.com/ProjectIdeas
If you are a physicists and have any ideas of what you would like formalizing, would love to hear them!
#physics #science
Some updates from PhysLean this week! All can be viewed here:
🔗 github.com/HEPLean/Phys...
#physics #science
🔗 github.com/HEPLean/Phys...
#physics #science
July 11, 2025 at 2:47 PM
Some updates from PhysLean this week! All can be viewed here:
🔗 github.com/HEPLean/Phys...
#physics #science
🔗 github.com/HEPLean/Phys...
#physics #science
July 4, 2025 at 3:16 PM
The Euler-Lagrange equations form the foundation to classical mechanics and are used in many other parts of #physics. Today, thanks primarily to Tomas Skrivan, we merged the proof of Euler-Lagrange equations from the principle of least action into PhysLean!
July 1, 2025 at 9:22 AM
The Euler-Lagrange equations form the foundation to classical mechanics and are used in many other parts of #physics. Today, thanks primarily to Tomas Skrivan, we merged the proof of Euler-Lagrange equations from the principle of least action into PhysLean!