32 lines
1,012 B
Markdown
32 lines
1,012 B
Markdown
# 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.
|