High Energy Physics in Lean

A project to digitalize high energy physics.

Aims of this project

• Use Lean to create an exhaustive database of definitions, theorems, proofs, and calculations in high energy physics.
• Make a library that is easy to use by the high energy physics community.
• Keep the database up-to date with developments in MathLib4.
• Create gitHub workflows of relevance to the high energy physics community.

Where to learn more

• Read the associated paper:

  https://arxiv.org/abs/2405.08863

• The documentation for this project is at:

  https://heplean.github.io/HepLean/

• Watch this overview of HepLean:

  https://www.youtube.com/watch?v=W2cObnopqas

• A list of 'Frequently asked questions' can be found on the Wiki for this project:

  https://github.com/HEPLean/HepLean/wiki/The-answers-to-some-questions

• Feel free to connect on the Lean Zulip channel:

  https://leanprover.zulipchat.com

• A small example script relating to the three fermion anomaly cancellation condition can be found here

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

Adding Lean Copilot (optional)

Lean Copilot allows the use of large language models in Lean. Using Lean Copilot with HepLean can be done in the following way:

Either:

• Run the script ./scripts/add-copilot.sh

Or:

• Copy the file ./scripts/copilot_lakefile.txt over to lakefile.lean,
• Run lake update LeanCopilot,
• Run lake exe LeanCopilot/download,
• Run lake build.

To use LeanCopilot add import LeanCopilot to the top of the lean file you are working in. The following commands should then become available to you:

• suggest_tactics,
• search_proofs,
• select_premises.

Adding Lean Copilot will modify a number of files. If you have added Lean Copilot, please do not push changes to the following files:

• lakefile.lean,
• .lake/lakefile.olean,
• .lake/lakefile.olean.trace,
• lake-manifest.json.

Please also ensure that there are not any import LeanCopilot statements in the lean files.