From fe0e3c3684746d682f2b31fa2fd354aba60b9cfa Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 20 Aug 2024 10:12:19 -0400 Subject: [PATCH] Update README.md --- README.md | 51 ++++++++++++++++++++++++++------------------------- 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/README.md b/README.md index f35a25c..ce374ef 100644 --- a/README.md +++ b/README.md @@ -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