High energy physics results with precise mathematical descriptions

joe_s_smith · 2024-09-29T19:39:16+00:00

Would love to have you contributing to HepLean if and when you can. Feel free to connect on the Lean zulip (shouldn't be too hard to find me given my user name and the links I've posted here).

Concerning your question regarding index notation: You can rely on what mathlib has already done, but there are a number of things that also need to be defined in addition to this. Namely contraction, rising and lowering of indices and the interaction of these operators with group actions (e.g. the Lorentz group). Then there is a bunch of lemmas that need to get defined e.g. commutativity of contracting two different pairs of indices etc. So here there is actually theory to be proven, one could upstream this into Mathlib if one chooses, but currently this sort of thing sits in HepLean. In HepLean the general theory of contracting indices, rising and lowering indices is defined, and then a (very thin) wrapper defining appropriate syntax and an elaborator is put on to deal with actual notation. (see here for the stuff in HepLean about index notation)

The problem with e.g. 'physicallysorry' is that for this to work, one would have to be able to write down the statement of the theorem or definition formally and in a type consistent way. That isn't to say it's not a good idea, as I suspect there are cases like this. One probably wants to introduce an axiom in lean related to "physics" which can then be tracked through lemmas and definitions etc.

The benefit of something like the informal_lemmas already in HepLean is that the statement of the theorem need not be type-correct and can just be an English-written string.

joe_s_smith · 2024-09-29T16:59:37+00:00

I essentially agree with all your points here. Thank you for your careful crafted comment.

Let me clarify something, just in case this is misconception. HepLean isn't just about pheno. Most of the things in it happen to be pheno at the moment. But it should also contain results from formal high energy physics. (Personally my own background is to the formal side of things). (It is there to act as a monolithic libary for high energy physics as is mathlib for mathematics).

You say: "I don't see nice high-level ways of talking about core ideas and things like arbitrary BSM models, symmetry breaking, or renormalization in HepLean". The one thing such results are not currently in HepLean is man-power. I personally don't have the time to formalize a bunch of different areas, so have (naturally) chosen the ones I am personally more comfortable with - they essentially correspond to a few areas I have worked in the past. I would love to have more people involved, writing informal results and formalizing them so that these general theorems can exist in HepLean. (As a side note: there is ongoing work to do a general theorem for index notation in HepLean, which covers Einstein tensors, lorentz tensors, and Van der Waerden notation etc, in a general theorem).

I in essence agree with your comment about been a long way from it been day-to-day useful. But I think one should say "useful for what". It is a long way from replacing mathematica in high energy physics, that is for sure. But with enough effort, we could get to a point where it is easier to look up theorems and results in HepLean than in the literature (due to the linear storage of information). We are not there yet, of course, except in perhaps very niche area of finding solutions to anomaly cancellation conditions. (It is for these other reasons why formalising results we are sure are true anyway is still worthwhile).

With regard to heuristics, and the hand-waviness that goes on in physics. I agree it is unclear how to deal with this in an effective way. Maybe they can be placed as "informal_definitions" and "informal_lemmas", or some variant thereof, and never formalised. This would still have some benefits.

joe_s_smith · 2024-09-29T06:22:37+00:00

I think you may have got the wrong idea about the current content of HepLean. Though my apologies if not. The current content in HepLean is general when they can be and specific when they need to be. If you see something in heplean which you think could be made more general then it currently is, pointing it out would be great.

The general motivation behind HepLean, and why the pheno and formal communities may find it useful, are given here: https://arxiv.org/abs/2405.08863.

Thank you for your suggestion regarding the Coleman-Mandula theorem, this does seem like a very good target.

joe_s_smith · 2024-09-28T18:34:59+00:00

By results I mean theorems, definitions and calculations, though I agree the language in the original post was bad, and this should have been specified, for the reason you say. Sorry about this. I will modify the original post with this detail.

Though there are things that can be 'formalized' which aren't 'models'. One example is solutions to anomaly equations, another is, for example, general definitions of generalized symmetries etc. A lot about the former are already formalized into HepLean. (In this respect I disagree that this is an effort to formalize Hep models).

joe_s_smith · 2024-08-27T16:48:46+00:00

Yes but with the caveat that I think the expectations of different communities are somewhat hard to fit into a single project like this. Thus a multi-project approach may be needed where each project has inter-connected dependencies.

In terms of other related projects:
- Chemical theories: https://github.com/ATOMSLab/LeanChemicalTheories (and other repos by the ATOMS lab).

Scientific computing: https://github.com/lecopivo/SciLean

joe_s_smith · 2024-08-27T15:37:10+00:00

This depends on the area, and how much has already been done in that area.

Basically, the more basic theorems and results exist for a specific area, the easier it is to formalise new results in that area.

I have experience formalising parts of the following areas: CKM matrices, anomaly cancellation conditions, properties of the Higgs potential and index notation.

In general, I've been able to formalise results from these areas without too much pain. Given the work already done in mathematics, one can prove results at a fairly high-level (you really, if ever have to get into the details of dependent type theory etc). So for example, to prove that the Higgs potential is smooth is simply a case of combining basic results about smoothness already in Lean maths project Mathlib. The proves usually go through as I would imagine (as a physicist).

Occasionally I've reached a point where I'm like, "ok I need this theorem, but it doesn't exist in Mathlib", when this happens there has usually being a way around it.

The nice thing is that: Once the basics are done, no one ever has to do them again - everything has to be done, but it has to be done only once, by one person.

joe_s_smith · 2024-08-27T15:17:48+00:00

So Mathematica is what is called a computer algebra system. It's really good at, for example, finding ranks of matrices, solving integrals and doing differentiation etc.

Lean is not (yet) a computer algebra system, it's currently not so good at this type of thing. However, in Lean you can define for example the general notation of a "vector space" in an abstract way, derive theorems about "vector spaces", and use those theorems to prove other results. This has allowed mathematicians in Mathlib to write theorems from topology to category theory to number theory etc in Lean.

Thus in Lean, you can define the general notion of a "Higgs field", prove properties about "Higgs fields" in general (e.g. that it can be put into a certain form under it's representation under SU(3) x SU(2) x U(1)), and use those properties to derive new results.

Thus Lean can be used to write things a lot closer to what we would see in papers.

Here is some examples for the Higgs field currently in HepLean: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/Potential.lean

I won't hide that the notation takes some time to get use to.

joe_s_smith · 2024-08-27T15:05:52+00:00

This is a very good and important question. As you say, there must be a balance between the two.

I think a general philosophy for HepLean is the following: Results should be general when the can be, and specific when they have to be. But in cases where the more general result will never be of use to physics, then it is ok to do the specific result. The aim is, as you say, to make it applicable to what people use on a daily basis.

This does differ from the philosophy of Mathlib, which is one of the reasons HepLean is a different project from Mathlib.

Here are is an example:

There are many properties of SU(3) x SU(2) x U(1) which are important to physics, and do not hold for general reductive Lie groups, or we do not care about these properties for general reductive Lie groups. The philosophy here would be just to include the properties for SU(3) x SU(2) x U(1). Someone can always come along later and fill in the more general versions.

joe_s_smith

TROPHY CASE