# High Energy Physics in Lean

## Aims of this project

- Use Lean to create a database of definitions, theorems and proofs 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/
- Feel free to connect on the Lean Zulip channel: 

  https://leanprover.zulipchat.com

## Contributing 

We follow here the same contribution policies as MathLib4. 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. 
2. Run `lake -Kenv=dev update`.

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