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:
jstoobysmith 2024-08-20 10:12:19 -04:00
parent 1370c9b055
commit fe0e3c3684
1 changed files with 26 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

51
README.md
View file

@ -10,10 +10,25 @@ A project to digitalize high energy physics.
## Aims of this project
- Use Lean to create an exhaustive database of definitions, theorems, proofs, and calculations in high energy physics.
- Make a library that is easy to use by the high energy physics community.
- Keep the database up-to date with developments in MathLib4.
- Create GitHub workflows of relevance to the high energy physics community.
1. 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,
with the potential future use of AI.
3. Create good documentation so that the project can be used for pedagogical purposes.
## Ideas for contributions
Any contribution to HepLean is more than welcome. However, if you would like to contribute but
are struggling to work out how, here are some potential starting points:
1. Prove further results related to the Lorentz group, the Poincare group and their algebras.
Despite some work has being done in this direction there is still much more to do.
2. Prove further results related to the two Higgs doublet model, or other BSM theories.
HepLean does not currently contain fermions (but soon will) so starting with the scalar potential
is a good start.
3. Tidy up the material on anomaly cancellation. Furthermore, there are results from the
literature in this area not already digitalized.
4. Make the first steps in digitalizing super-symmetry, the Randall-Sundrum model etc.
## Areas of high energy physics with some coverage in HepLean
@ -24,27 +39,13 @@ A project to digitalize high energy physics.
[![](https://img.shields.io/badge/Lorentz_Group-blue)](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html)
[![](https://img.shields.io/badge/Anomaly_Cancellation-blue)](https://heplean.github.io/HepLean/docs/HepLean/AnomalyCancellation/Basic.html)
[![](https://img.shields.io/badge/Feynman_diagrams-blue)](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/PhiFour/Basic.html)
## Where to learn more
- Read the associated paper:
https://arxiv.org/abs/2405.08863
- The documentation for this project is at:
https://heplean.github.io/HepLean/
- Watch this overview of HepLean:
https://www.youtube.com/watch?v=W2cObnopqas
- A list of 'Frequently asked questions' can be found on the Wiki for this project:
https://github.com/HEPLean/HepLean/wiki/The-answers-to-some-questions
- Feel free to connect on the Lean Zulip channel:
https://leanprover.zulipchat.com
- A small example script relating to the three fermion anomaly cancellation condition can be found [here](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)
## 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 |
## Contributing