Scope

Stream: PhysLean

[Joseph Tooby-Smith]

One of the questions I have been asked frequently, especially recently, is about the scope of HepLean.

As a guide, I was thinking of a page like
this but for physics and covering graduate as-well as undergraduate areas, and clearly indicating what is in scope and what currently (if anything) isn't .

This has the added benefit of allowing people to see what has already been formalized and what else is 'left' to be done.

For graduate physics I think the Cambridge part III course is a natural go-to as a starting point.
For undergraduate math, mathlib used this as a starting point. I'm yet to find something as detailed for undergraduate physics. Although my french is non-existent to such a thing may exist.

If anyone has any thoughts on what should be or shouldn't be in scope let me know, or any other suggestions relating to this!

[Kevin Buzzard]

That undergraduate math page has become a bit of a millstone around our neck. The history of the page was that back in the 2010s one of the main goals was for mathlib to cover an undergraduate curriculum because without that we could do nothing, and the computer scientists I spoke to (in the 2010s the area was dominated by computer scientists) either seemed to think that this had "surely been achieved by now" or were not remotely interested in achieving it. But there were complaints that "an undergraduate degree" was quite an ill-specified goal; my working definition at that time was "all the theorems in all the courses I was taught in my final year undergrad in Cambridge in 1989/90" but I would never write down exactly what this was so Patrick Massot (who had access to a very precise document containing exactly the syllabus of one of the degree courses at his university) just wrote down what was on that. The problem with the list is that there are things on it which we don't really want, or even worse which we don't particularly want but if we do get it then we know exactly what form we want it in and it would be very technical to do and certainly not a project for a beginner -- but somehow are now stuck asking for them and beginners come along and say "I'd like to help by doing this one" and the response is "yeah but unfortuntely this is 100 times more difficult than it looks". So let that be a cautionary tale!

[Joseph Tooby-Smith]

Ok, maybe taking heed to this caution is smart then.
Perhaps a more curated list (without making reference to the graduate or undergraduate curriculum) would overcome at least some of these problems, whilst still giving people an idea of scope of the project.

[Tyler Josephson ⚛️]

I think a “blueprint” style is more helpful, because that aims to line up dependencies in a way that doesn’t happen from a list of topics. But, since we haven’t solved Hilbert’s 6th problem, it may fruitful to propose multiple blueprints that intersect informally.

[Tyler Josephson ⚛️]

Will condensed matter physics be in scope? You’ve mentioned that “high energy physics” might be a misnomer; if you don’t intend to limit the scope, maybe a broader name would be better?

[Tyler Josephson ⚛️]

What about something like Flory-Huggins?

[Tyler Josephson ⚛️]

How about Hartree-Fock?

[Joseph Tooby-Smith]

So for the blueprint side of things. HepLean already has something like this here (it doesn't render very well on the website - sorry), but designed to work more closely with a project like Mathlib.

I agree a series of blueprints after specific targets would be useful, but I think solve a slightly different goal to what I am trying to solve here.

[Joseph Tooby-Smith]

In terms of scope, I think it is important to ask what is most useful.

I think most of us agree that there are good reasons not to clump a Lean physics project with Mathlib.
And just because all of mathematics fits nicely in a single project does not imply that this is necessarily true for physics.

In particular I think there are a series of core fundamental areas of physics, for example:

• relativity
• particle physics
• quantum mechanics (including things like the second quantization)
• quantum field theory
• classical mechanics and field theory
• cosmology
• thermodynamics
• ....

To one extent or another, these are all part of High energy physics, and I feel would fit in the scope of a project like HepLean.

There are other parts of physics which sit slightly apart from the list I gave above:

• Aspects of condensed matter physics (not included above)
• Fluid dynamics
• Astrophysics
• Plasma physics
• Biophysics
• Polymer physics
• ...

For these areas it is less clear to me that they should sit in e.g. HepLean. This is mainly because the focus is different, the communities are different and the techniques used are different.

[Joseph Tooby-Smith]

Maybe all of this is said more succinctly by saying that IMHO, HepLean should cover results from and the foundations of the following arXiv categories:

• hep-th: High Energy Physics - Theory
• hep-ph: High Energy Physics - Phenomenology
• hep-ex: High Energy Physics - Experiment
• hep-lat: High Energy Physics - Lattice
• gr-qc: General Relativity and Quantum Cosmology
• math-ph: Mathematical Physics

[Joseph Tooby-Smith]

Having thought a bit more about this I would like to add the following: I think there will be a point where the scope of HepLean should and will be expanded (and its named changed), but I think this will come naturally, when a lot more of the foundations (e.g. QM, special relativity etc) are in HepLean and there are a lot more active contributors.

[Winston Yin (尹維晨)]

Hi Joseph, as a particle cosmologist with some experience in high energy physics and mathematical physics, I've been interested in following this project for some time now. I've also been thinking what the goal of this kind of physics formalisation project should be, so I'm curious what you think.

In the case of mathlib, Kevin has repeatedly advertised it as something that can become increasing useful to working mathematicians, with one possibility that research-level maths can be routinely formalised as part of the publishing process to ensure correctness and expedite review. Formalisation also helps to clarify and distill certain informal arguments. The goal of mathlib, then, seems aligned with a vision for the future of mathematics, and mathematicians generally should therefore care about it.

There are many well established mathematical frameworks for physics that have not been formalised in Lean yet, and you have listed several of these. Of course, one can simply march ahead and start formalising them. However, working physics is very different from working mathematics. Most physicists, including hardcore theorists, do not care for formal rigour in their mathematical arguments. Most results in high energy physics are not stated with enough rigour to even be formalised in principle (such as most submissions to all but the last arXiv category you listed). Is our audience mainly mathematical physicists? What are some reasons a working physicist should care about formalised physics?

My specialty is in theoretical cosmology, where we rely heavily on heuristic arguments, order-of-magnitude estimates, and simulations. I can see some derivations that can in principle be formalised, but then I'm faced with the question of what value is added to my research by this. I hope this doesn't come off as sceptical or dismissive. I'm personally interested in this because of my interest in mathematical physics, and I think physics provides a testing ground for the user experience of machine assisted formalised derivations. If the audience of this project are mainly mathematical physicists, it'll already be quite valuable. Since this is called HepLean, I would just like to be realistic about the kinds of HEP people who might find this interesting / useful, so as to better define the scope of this project.

[Winston Yin (尹維晨)]

By the way, I have been contributing to parts mathlib on ODEs and manifolds. I'm motivated by the hope of seeing the Einstein Field Equations or the Yang-Mills Lagrangian stated through mathlib's diff geo library, so I think our goals are aligned in some direction.

[Winston Yin (尹維晨)]

And congratulations on your Computer Physics Communications paper. Perhaps you've explained much of this there, and I'll give it a read.

[Joseph Tooby-Smith]

Hi @Winston Yin (尹維晨) great question!

Let me start with stating that I disagree with this sentence:

Most results in high energy physics are not stated with enough rigour to even be formalised in principle

Or rather, I disagree with the conclusion. Lots of results in HEP may not be stated with enough rigour that one can take a paper and just formalize it in the same way that you can in maths, but that doesn't mean it can't be formalized at all. Indeed there are currently research level results in HepLean.

In terms of why it might be useful to the working physicist I think there are a number of reasons:

1. Allows easier look up and cataloging of information.
2. Allows you to be sure of results from the area.
3. Allows you to use new automated methods (e.g. machine learning) to prove theorem AND do calculations (which are just fancy theorems).
4. Allows for new pedological methods.
5. Allows you a way to interface between theory, programs and simulations - if the definitions are done correctly. (this is one of the places I see HepLean differing from Mathlib in nature)

These are discussed in more detail in the paper I link to, and there are probably more I've missed.

String theorists are particularly interested in 3 and I have investigated/ am investigating this with some of them.

The benefits I list above may not be realized in 1 year or even 10 years, but I'm pretty confident they will be one day. In particular even now there are lots of things you can do in Lean that you can't do in say Mathematica.

To answer your question more directly: I see this project of been of interest to the mathematical physicist for the natural reason, and been of interest to the 'working' physicist for the reasons I outline above.

[Joseph Tooby-Smith]

Concerning "heuristic arguments" and "order-of-magnitude estimates" either including these in strings or where necessary as assumptions in theorems is one way around this. But these are indeed a challenge that need a satisfactory solution. I'm optimistic we will find one either naturally through the process of formalization or forced.

[Joseph Tooby-Smith]

Part of the most important work that can be done in HepLean now is making it as easy as possible and as fruitful as possible for the working physicist - even those that don't learn Lean. I discussed more in this direction in my Lean together talk.
In this regard I have already included index notation (see here).

[Winston Yin (尹維晨)]

Thanks for the answer! I’m optimistic that it can be very fruitful.