A project to digitalize physics.

(Formerly called HepLean)

Aims of this project

🎯 Digitalize results (meaning calculations, definitions, and theorems) from physics into Lean 4.

🎯 Develop structures to aid the creation of new results in physics using Lean, with the potential future use of AI.

🎯 Create good documentation so that the project can be used for pedagogical purposes.

Some parts of PhysLean

PhysLean currently includes, but is not limited to, the following parts:

Lorentz 🗂️: The Lorentz group, Lorentz algebra, Weyl fermions, Real Lorentz vectors, complex Lorentz vectors, complex Lorentz tensors, bispinors, Pauli matrices, etc.

Index notation 🗂️ 📄: Formalization of index notation using category theory allowing commands like

{A | μ ν ⊗ S | μ ν = - A | μ ν ⊗ S | μ ν}ᵀ

Anomaly cancellation 🗂️: Results related to solutions to the anomaly cancellation conditions of several theories.

Standard Model physics 🗂️: Properties of the Higgs potential.

BSM physics 🗂️: Starts to: Georgi Glashow model, Pati-Salam, Spin(10), Two Higgs doublet model.

Flavor physics 🗂️: Properties of the CKM matrix.

Perturbation Theory 🗂️: Time-dependent version of Wick's theorem for both fermions and bosons.

Associated media and publications

• 📄 Joseph Tooby-Smith, HepLean: Digitalising high energy physics, Computer Physics Communications, Volume 308, 2025, 109457, ISSN 0010-4655, https://doi.org/10.1016/j.cpc.2024.109457. [arXiv:2405.08863]
• 📄 Joseph Tooby-Smith, Formalization of physics index notation in Lean 4, arXiv:2411.07667
• 💻 Example code snippet related to Anomaly cancellation conditions.
• 🎥 Seminar recording of "HepLean: Lean and high energy physics" by J. Tooby-Smith

Papers referencing PhysLean

• Hu, Jiewen, Thomas Zhu, and Sean Welleck. "miniCTX: Neural Theorem Proving with (Long-) Contexts." arXiv preprint arXiv:2408.03350 (2024). Project page

How HepLean was used: Theorems from the space-time files of HepLean were included in a data set used to evaluate the ability of models to prove theorems from real-world repositories, which requires working with definitions, theorems, and other context not seen in training.

Contributing

We would love to have you involved! See the Get Involved page to see how you can get involved. Any contributions are welcome! If you have any questions or want permission permission to create a pull-request for this repository contact Joseph Tooby-Smith on the Lean Zulip, or email.

Installation

If you want to play around with HepLean, but do not want to download Lean, then you can use GitPod.

Installing Lean 4

Installation instructions for Lean 4 can be found:

• https://lean-lang.org/lean4/doc/quickstart.html

or

• https://leanprover-community.github.io/get_started.html

Installing PhysLean

• Clone this repository (or download the repository as a Zip file)
• Open a terminal at the top-level in the corresponding directory.
• Run lake exe cache get. The command lake should have been installed when you installed Lean.
• Run lake build.
• Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor).

Optional extras

• Lean Copilot and LLMLean allow for the use of large language models in Lean
• tryAtEachStep allows one to apply a tactic, e.g. exact? at each step of a lemma in a file to see if it completes the goal. This is useful for golfing proofs.