High Energy Physics in Lean

Aims of this project

• Use Lean to create a exhaustive database of definitions, theorems, proofs and calculations in high energy physics.
• Keep the database up-to date with developments in MathLib4.
• Create github workflows of relevence to the high energy physics community.

Where to learn more

• The documentation for this project is at:

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

• 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). With the exception that we allow some sorry statements, if a theorem is widly expected to be true by the community.

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

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

Quick installation

1. Clone this repository.
2. Open a terminal in the cloned directory.
3. Run lake -Kenv=dev update.

Depending on how up to date this directory is compared to MathLib4 this may lead to errors.