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

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.

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.

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

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

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

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!