A project to digitalize high energy physics.
- Digitalize results (meaning calculations, definitions, and theorems) from high energy physics into Lean 4.
- Develop structures to aid the creation of new results in high energy physics using Lean, with the potential future use of AI.
- Create good documentation so that the project can be used for pedagogical purposes.
| Description | |
|---|---|
| Paper | HepLean: Digitalising high energy physics |
| Code | Example code snippet |
| Video | HepLean: Lean and high energy physics |
| Video | Index notation in Lean 4 |
- Hu, Jiewen, Thomas Zhu, and Sean Welleck. "miniCTX: Neural Theorem Proving with (Long-) Contexts." arXiv preprint arXiv:2408.03350 (2024).
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.
The installation instructions for Lean 4 are given here: https://leanprover-community.github.io/get_started.html.
- 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 commandlakeshould 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).
- Lean Copilot allows the use of large language models in Lean.
- tryAtEachStep allows one to apply a tactic, e.g.
exact?at each step of a lemma in a file to see if it completes the goal. This is useful for golfing proofs.
