PhysLean

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

Public view of Lean | Zulip team chat Browse the publicly accessible channels in Lean without logging in.

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

YouTube video by Joseph Tooby-Smith Tutorial: Golfing proofs in PhysLean

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.

YouTube video by Joseph Tooby-Smith Tutorial: Adding Informal Results to PhysLean

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

YouTube video by Joseph Tooby-Smith Defining time in PhysLean

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

physlean.com

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!

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!

Weekly updates from PhysLean:

In short: We had the first steps towards an API for distributions for physicists, some work done in F-theory, and some cleaning up of the code base and website.

#physics #lean

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

Some updates from PhysLean this week! All can be viewed here:

🔗 github.com/HEPLean/Phys...

#physics #science

New things from the last week in PhysLean:

#physics

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!

Pleased to see that PhysLean has appeared in this paper:

🔗https://arxiv.org/abs/2506.16596

On knowledge resources for AI.

💻 Updates to the PhysLean Website

physlean.com

The PhysLean website has been updated to make it easier to navigate to various parts of the project including:

- getting started page,
- loogle search for PhysLean,
- online playground,
- Zulip discussion forum,
- and more!

#physics

YouTube video by Joseph Tooby-Smith PhysLean: Questions and answers about the project

Want to learn more about PhysLean and what the project is about, and the motivations behind it?

Take a look at this video:

www.youtube.com/watch?v=Q4HZ...

GitHub - HEPLean/PhysLean: A project to digitalise results from physics into Lean. A project to digitalise results from physics into Lean. - HEPLean/PhysLean

This is a new account for news related to the project PhysLean. A project to digitalize #physics results into the interactive theorem prover Lean 4.

See the link below if you are interested in the project:

github.com/HEPLean/Phys...