Reservoir

A project to digitalize high energy physics.

Aims of this project

1. Digitalize results (meaning calculations, definitions, and theorems) from high energy physics into Lean 4.
2. Develop structures to aid the creation of new results in high energy physics using Lean, with the potential future use of AI.
3. Create good documentation so that the project can be used for pedagogical purposes.

Ideas for contributions

Any contribution to HepLean is more than welcome. However, if you would like to contribute but are struggling to work out how, here are some potential starting points:

1. Prove further results related to the Lorentz group, the Poincare group and their algebras. Despite some work has being done in this direction there is still much more to do.
2. Prove further results related to the two Higgs doublet model, or other BSM theories. HepLean does not currently contain fermions (but soon will) so starting with the scalar potential is a good start.
3. Tidy up the material on anomaly cancellation. Furthermore, there are results from the literature in this area not already digitalized.
4. Make the first steps in digitalizing super-symmetry, the Randall-Sundrum model etc.

Areas of high energy physics with some coverage in HepLean

Associated media and publications

Contributing

We follow here roughly the same contribution policies as MathLib4 (which can be found here).

A guide to contributing can be found here.

If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email.

Installation

Installing Lean 4

The installation instructions for Lean 4 are given here: https://leanprover-community.github.io/get_started.html.

Installing HepLean

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