2024-04-16 16:23:49 -04:00
# High Energy Physics in Lean
2024-04-21 16:58:14 -04:00
## Aims of this project
2024-04-17 06:38:25 -04:00
2024-04-22 07:01:50 -04:00
- Use Lean to create a exhaustive database of definitions, theorems, proofs and calculations in high energy physics.
2024-04-17 06:38:25 -04:00
- Keep the database up-to date with developments in MathLib4.
- Create github workflows of relevence to the high energy physics community.
2024-04-16 16:23:49 -04:00
2024-04-21 16:58:14 -04:00
## Where to learn more
2024-04-17 08:48:09 -04:00
2024-04-21 16:58:14 -04:00
- The documentation for this project is at:
2024-04-21 16:59:00 -04:00
2024-04-21 16:58:14 -04:00
https://heplean.github.io/HepLean/
- Feel free to connect on the Lean Zulip channel:
2024-04-21 16:59:00 -04:00
2024-04-21 16:58:14 -04:00
https://leanprover.zulipchat.com
2024-04-16 16:23:49 -04:00
## 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.
