Skip to the content.
Screenshot of Wick's theorem implementation in PhysLean

The above screenshot demonstrates how theorems are formalized in PhysLean.

PhysLean was formerly called HepLean

1. Mission of PhysLean

To create a library of digitalized physics results in the theorem prover Lean 4, in a way which is useful to the broad physics community.

2. Vision of PhysLean

Statement: PhysLean aspires to be the definitive library for physics in Lean, akin to Mathlib for mathematics, with both the Lean and physics communities behind it and a potential formal collaboration.

Detailed Vision:

3. Values of PhysLean

The three core values of PhysLean are:

4. Potential impact of the PhysLean

PhysLean has the potential to have the following impact on the physics community:

5. Benifits of a monolothic libary

PhysLean is a monolithic library for physics, similar to how Mathlib serves mathematics. It aims to cover the entire field of physics within a single, unified framework. Here are some key motivations for adopting a monolithic approach:

6. Where to learn more

You can learn more about PhysLean by reading: 2405.08863, or contacting Joseph Tooby-Smith at: joseph at heplean dot com.