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:

• A comprehensive repository for containing fundamental definitions, theorems, and calculations from physics.
• A interface between experimental data, simulations, and formal theoretical frameworks.
• Extensive, physics-focused documentation to support adoption.
• Accessibility for physicists at all levels, including and especially to those new to formal methods.
• An intuitive set-up that aligns with the way physicists think and work.
• A large and active team, with the potential for structured, high-energy physics-style collaborations.

3. Values of PhysLean

The three core values of PhysLean are:

• Welcoming: PhysLean strives to foster an environment where contributors of all academic backgrounds and experience levels feel valued, supported, and empowered to make meaningful contributions.
• Open and Transparent: PhysLean and its outputs will always be openly accessible, freely available, and developed with transparency to benefit the broader physics and Lean communities.
• Accessibility and Practicality: PhysLean is designed to be intuitive, well-documented, and directly useful to physicists, regardless of their familiarity with formal methods.

4. Potential impact of the PhysLean

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

• Make it easier to find results.
• Make it easier to automate the creation of new results using e.g. machine learning methods.
• Make it easier to check papers and results for mathematical correctness.
• Create new avenues through which physics can be taught.
• Open up new ways to interface between theory and computer programs.

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:

• Prevents duplication of work: A single, comprehensive library ensures that contributors don’t waste effort reinventing the wheel.
• Facilitates shared improvements: When everyone works within the same library, enhancements to one part can be easily propagated to others.
• Simplifies maintenance: A unified library keeps everything up to date together. Individual contributors don’t have to manually update their code to stay compatible with new versions of Mathlib or other dependencies—that responsibility is shared by the community.
• Encourages standardization: A single library fosters consistency in notation, conventions, and methodology, reducing fragmentation in the ecosystem.
• Improves discoverability and usability: With all physics in one place, users can more easily find and apply existing results rather than searching through scattered libraries.

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.