DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update README.md

Browse source
This commit is contained in:
Joseph Tooby-Smith 2024-11-11 05:37:29 +00:00 • committed by GitHub
parent 7dc0a264f3
commit eaf9a0364e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 19 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

31
README.md
View file

@ -12,15 +12,17 @@ A project to digitalize high energy physics.
## Aims of this project
1. Digitalize results (meaning calculations, definitions, and theorems) from high energy physics
🎯 __Digitalize__ results (meaning calculations, definitions, and theorems) from high energy physics
into Lean 4.
2. Develop structures to aid the creation of new results in high energy physics using Lean,
🎯 Develop structures to aid the __creation__ of new results in high energy physics using Lean,
with the potential future use of AI.
3. Create good documentation so that the project can be used for pedagogical purposes.
🎯 Create good documentation so that the project can be used for __pedagogical__ purposes.
## Some parts of HepLean
HepLean _currently_ includes but is not limited to the following parts:
HepLean _currently_ includes, but is not limited to, the following parts:
__Lorentz [🗂️](https://heplean.github.io/HepLean/docs/HepLean/Lorentz/Group/Basic.html):__ The Lorentz group, Lorentz algebra, Weyl fermions, Real Lorentz vectors, complex Lorentz vectors, complex Lorentz tensors, bispinors, Pauli matrices, etc.
@ -39,12 +41,9 @@ __BSM physics [🗂️](https://heplean.github.io/HepLean/docs/HepLean/BeyondThe
__Flavor physics [🗂️](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html):__ Properties of the CKM matrix.
## Associated media and publications
| | Description |
|----|------|
| [Paper](https://arxiv.org/abs/2405.08863) | HepLean: Digitalising high energy physics |
| [Code](https://live.lean-lang.org/#code=import%20Mathlib.Tactic.Polyrith%20%0A%0Atheorem%20threeFamily%20(a%20b%20c%20%3A%20ℚ)%20(h%20%3A%20a%20%2B%20b%20%2B%20c%20%3D%200)%20(h3%20%3A%20a%20%5E%203%20%2B%20b%20%5E%203%20%2B%20c%20%5E%203%20%3D%200)%20%3A%20%0A%20%20%20%20a%20%3D%200%20∨%20b%20%3D%200%20∨%20c%20%3D%200%20%20%3A%3D%20by%20%0A%20%20have%20h1%20%3A%20c%20%3D%20-%20(a%20%2B%20b)%20%3A%3D%20by%20%0A%20%20%20%20linear_combination%20h%20%0A%20%20have%20h4%20%3A%20%203%20*%20a%20*%20b%20*%20c%20%3D%200%20%3A%3D%20by%20%0A%20%20%20%20rw%20%5B←%20h3%2C%20h1%5D%0A%20%20%20%20ring%20%0A%20%20simp%20at%20h4%20%0A%20%20exact%20or_assoc.mp%20h4%0A%20%20%0A) | Example code snippet |
| [Video](https://www.youtube.com/watch?v=W2cObnopqas) | HepLean: Lean and high energy physics |
| [Video](https://www.youtube.com/watch?v=IjodVUawTjM) | Index notation in Lean 4 |
- [📄](https://arxiv.org/abs/2405.08863) Joseph Tooby-Smith, __HepLean: Digitalising high energy physics__, arXiv:2405.08863
- [💻](https://live.lean-lang.org/#code=import%20Mathlib.Tactic.Polyrith%20%0A%0Atheorem%20threeFamily%20(a%20b%20c%20%3A%20ℚ)%20(h%20%3A%20a%20%2B%20b%20%2B%20c%20%3D%200)%20(h3%20%3A%20a%20%5E%203%20%2B%20b%20%5E%203%20%2B%20c%20%5E%203%20%3D%200)%20%3A%20%0A%20%20%20%20a%20%3D%200%20∨%20b%20%3D%200%20∨%20c%20%3D%200%20%20%3A%3D%20by%20%0A%20%20have%20h1%20%3A%20c%20%3D%20-%20(a%20%2B%20b)%20%3A%3D%20by%20%0A%20%20%20%20linear_combination%20h%20%0A%20%20have%20h4%20%3A%20%203%20*%20a%20*%20b%20*%20c%20%3D%200%20%3A%3D%20by%20%0A%20%20%20%20rw%20%5B←%20h3%2C%20h1%5D%0A%20%20%20%20ring%20%0A%20%20simp%20at%20h4%20%0A%20%20exact%20or_assoc.mp%20h4%0A%20%20%0A) Example code snippet related to Anomaly cancellation conditions.
- [🎥](https://www.youtube.com/watch?v=W2cObnopqas) Seminar recording of "HepLean: Lean and high energy physics" by J. Tooby-Smith
### Papers referencing HepLean
- Hu, Jiewen, Thomas Zhu, and Sean Welleck. "miniCTX: Neural Theorem Proving with (Long-) Contexts." arXiv preprint [arXiv:2408.03350](https://www.arxiv.org/abs/2408.03350) (2024). [Project page]( https://cmu-l3.github.io/minictx/)
@ -57,13 +56,21 @@ We follow here roughly the same contribution policies as MathLib4 (which can be
A guide to contributing can be found [here](https://github.com/HEPLean/HepLean/blob/master/CONTRIBUTING.md).
If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email.
If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the [Lean Zulip](https://leanprover.zulipchat.com), or email.
## Installation
If you want to playaround with HepLean, but do not want to download Lean, then you can use [GitPod](https://gitpod.io/#https://github.com/HEPLean/HepLean).
### Installing Lean 4
The installation instructions for Lean 4 are given here: https://leanprover-community.github.io/get_started.html.
Installation instructions for Lean 4 can be found:
- https://lean-lang.org/lean4/doc/quickstart.html
or
- https://leanprover-community.github.io/get_started.html
### Installing HepLean