How to get the Lean community involved formalising physics?

Stream: general

[Joseph Tooby-Smith]

Those who frequent the Natural Sciences channel may know that I’m working on a project HepLean to formalise high energy physics into Lean. 

There are three sets of people who may be interested in getting involved in such a project:

1. High energy physicists. 
2. Mathematicians with a general interest in Lean and physics. 
3. Computer scientists with a general interest in Lean and physics.  

I’m working with people from the high energy physicists community with the aim of getting more people from set 1 involved, using e.g. physics-focused Lean blueprints. 

Here I would like input from the community on how I can get more people from sets 2 and 3 involved in this, or similar science-orientated projects? 

In other words, what would make you, dear reader, more likely to, and want to, contribute to this, or similar science-orientated projects? 

Some ideas I’ve had:

1. A TODO list of things that need doing in the project. (this can be found here)
2. A list of mathematical-orientated physics papers which would be nice to formalise. (including for example: this paper)

[Kim Morrison]

Given the preponderance of mathematicians in the existing user base, I think it would be helpful to have one or more roadmaps where the content "is clearly maths" but the destination is physics.

It's an honest mathematical theorem to describe the electron states in a hydrogen atom. What would we need to get there? etc

[Joseph Tooby-Smith]

Thanks @Kim Morrison! This is a nice suggestion :), and I will see what I can do in that direction.

[Tyler Josephson ⚛️]

I’m planning on making a similar blueprint for a chemical engineering thermodynamics class of problems. In this, we want more than just proofs, but executable programs, as well, so certain data-science-oriented tools in Lean will be on our To Do list, too.

[Tyler Josephson ⚛️]

Consider advertising this in the https://leanprover.zulipchat.com/#narrow/stream/445230-Lean-for-Scientists-and-Engineers-2024 channel, too! Some who took the course might appreciate ideas on how they can contribute to projects like HepLean.

[Kim Morrison]

Thermodynamics worries me a bit, as it is very hard to connect to foundations, so it's unclear whether you're doing physics or just "manipulating symbols". :-)

[Patrick Massot]

Why do you say that? Isn’t thermodynamics all about differential forms?

[Kim Morrison]

Hmm, maybe, I guess I only ever learnt thermodynamics before I learnt maths, and never went back to see how you're meant to do it. :-)

[Joseph Tooby-Smith]

I have been thinking about how to implement something along the lines of Kim’s suggestion above in a project like HepLean.

Here is one plan:
In addition to lemma and definition etc, the commands informal_lemma and informal_definition. With, for example,informal_lemma containing the information of a physics statement of the lemma as a LaTeX string, a self-contained math statement of the lemma as a  LaTeX string, and a list of informal and formalized dependencies. This is similar to "proof_wanted" except even more informal.

Such informal_lemma's and informal_definition's would be placed in Lean code at the expected place the formal versions would be expected to appear. A script similar to the script which makes blueprints could be used to nicely display the informal definitions and lemmas (perhaps alongside formal versions).

I'm sure something like this has been proposed before. My hope is that it could provide something like the roadmaps Kim mentioned above, in a way that is more integrated with the Lean code.

Do people think such an idea would work and be useful, with regard to my initial comment above?

[Kim Morrison]

(To be clear, I wasn't suggesting anything informal. I wanted to define -∇^2 - 1/r as unbounded operator on L^2(R^3), etc. There's plenty of room in just a doc-string to say "This is the Schrodinger operator for hydrogen.")

[Joseph Tooby-Smith]

My comment is referring to the roadmaps, i.e. before formalisation has taken place. So e.g. initially there would be something like:

informal_definition hydrogen_schrodinger_operator := "The Schrodinger operator for hydrogen defined as an unbounded operator on L^2(R^3)."

Then later someone can come along and make this a formal definition

/-- The is the Schrodinger operator for hydrogen. -/
def hydrogen_schrodinger_operator : L^2(R^3) := ...

I.e. the informal_definitions etc would form the roadmap.

[Joseph Tooby-Smith]

Or more in line what I'm thinking the informal definition could be something like:

informal_definition hydrogen_schrodinger_operator where
   physics := "The Schrodinger operator for hydrogen"
   math := "The unbounded operator on L^2(R^3), defined as  -∇^2 - 1/r"
   dependencies := [wavefunction]

[Yoh Tanimoto]

I think I belong to 2 (I would call myself a mathematical physicist but surely not a high-energy physicist). I find the general idea of your project interesting, and to attract more people, it is somewhat similar to Kim's suggestion but I think it would be nice to have a clear documentation, rather than codes, of what results you would like to have in Lean and what math you need to formalise them.

For example, I see an entry called StandardModel, but what are the actual mathematical contents? Do you want to write down the (classical) action? Do you want to define the scattering amplitudes in QED as formal series? It would be helpful to have (human-language) statements first.

[Joseph Tooby-Smith]

@Yoh Tanimoto Would my suggestion above provide sufficient such documentation? I'm imagining the informal definitions and lemmas to be turned into a blueprint type human-language webpage. (Just the documentation source code itself would form part of the Lean code).

Actually I don't think there is a command called StandardModel yet in HepLean, though there is a namespace which contains some properties of the standard model, like the Higgs field. But I understand your point.

[Yoh Tanimoto]

well, the format is ok. What I would like to see is more of a general line like what are the main definitions/results of the whole project.

[Joseph Tooby-Smith]

Ok, thanks this makes sense.

The project is meant to mirror Mathlib, rather than, for example the Fermat Last Theorem project. I.e. there is not a single target, but a more broad aim of generalising (any) results from high energy physics, and having a place to put foundational definitions and results.

For example, if someone wants to formalise the classical action of the Standard Model, or define scattering amplitudes for QED, or show that certain beyond-the-standard-model models are bounded etc, HepLean would be a good place to put them. There are no preset targets.

At least this is the aim of the project. However, I have thought about creating a list of possible targets people could aim for if they are interested in contributing to HepLean.

[Joseph Tooby-Smith]

(In other words HepLean is meant to be a monolithic project for formalising high energy physics, allowing one to connect different parts of the field together, and removing the need to reproduce results in different places.)

[Yoh Tanimoto]

I see. Still, I think it's good to show what the standard model should look like and how practical calculations work in Lean (it's "standard"!).

[Joseph Tooby-Smith]

This is something I am interested in doing. But we are still a long way from that point. Namely, we still need good definitions of fermions, good definitions of a gauge group, of a feynman diagram etc, before we can write down the correct formulation of, for example, the classical action of the standard model. (I note things like the Higgs potential are already in HepLean). I.e. there is lots to do, and any help is appreciated!

I'm hoping something like Kim or my suggestion above will increase progress in this direction. (I note though, there is a lot more to High energy physics than the standard model which may be worth formalising, for example TFTs, CFTs etc. HepLean is by no means restricted to standard-model physics or phenomenology.)

[Yoh Tanimoto]

Absolutely, and exactly for this, I thought writing some important stuff in the human language would be quicker and helpful

[Pietro Monticone]

@Joseph Tooby-Smith Thank you for sharing your proposal. I'm trying to fully understand your idea. Could you please clarify the benefits of incorporating informal_definitions and informal_lemmas into the Lean code of a blueprint-driven project, especially considering how the blueprint currently works?

[Joseph Tooby-Smith]

@Pietro Monticone I'm not proposing informal_definitions and informal_lemma, I'm proposing them for Mathlib style projects, where one wants to indicate theorems and definitions to be formalized and their interdependencies.

Here are the benefits I see:

1. Everything is in one place: The informal commands will appear right next to the formal ones. One does not need to open a separate repo, or even file, to edit and see the informal commands.
2. Varies backends for displaying the informal commands: The informal commands could be displayed using something like the current blueprint infrastructure, or some other infrastructure which can display them. The user writing these informal commands would not have to worry about what back-end code is being applied to them.
3. Location information: The informal commands will appear where their formalized versions are to appear. They can be moved around and refactored in the same way as formalized commands.

I see the informalized commands being deleted once the corresponding formal command has been made. The content of the informal command could be placed in the doc-string of the formal commands.

[Pietro Monticone]

Oh, now I see what you mean. Thanks for the clarification.

[Jineon Baek]

I am a pure math researcher and don't know much about theoretical physics. A huge benefit of formalization for mathematicians is that one can be sure that all math are consistent (we don't say x=+1 here and x=-1 there). The idea of having a single consistent theory with solid mathematical ground may attract more math oriented people, especially after making them 'uncomfortable' by showing some inconsistent calculations from research level physics and potential issues arised from that - are there any?

[Joseph Tooby-Smith]

@Jineon Baek Given that papers in high energy physics are rarely, if ever, reviewed for mathematical correctness - the answer to this is yes. Even some of my own papers, I've - post publication - discovered that I've overlooked a mathematical caveat and had to go back and prove a bunch of things to make sure what I was doing was correct.

I also expect there are examples which have cost a lot of money and a lot of research hours. B-anomalies in particle phenomenology are somewhat an example of this.

There are often debates in high energy physics about missing minus signs or factors of two etc, some of which make it into comments on the arXiv. At some point I would like to do a project which sorts out such a debate or finds an inconsistency using Lean. Anyone in helping with such a project should let me know :).

[Joseph Tooby-Smith]

For this informal_definition and informal_lemma thing. An example of such an implementation is here:

https://github.com/HEPLean/HepLean/pull/152/files

[Joseph Tooby-Smith]

(I should also note that I'm hoping that these informal_definition and informal_lemma will allow physicists who aren't so interested in learning Lean get more involved).

[mars0i]

@Joseph Tooby-Smith, for whatever it's worth, I think that there may be some philosophers of physics who might be very interested in this project and its goals. Not necessarily to help with proofs, but maybe that too. They might just be interested in paying attention to what's being done in this project. My area is philosophy of biology, but if you think it might be worthwhile, I would ask around with philosophers of physics.

[Joseph Tooby-Smith]

Hey @mars0i ! I think this is a great idea! I personally don't have any philosophers of physics in my network, if you happen to know any letting them know about this project would be great!

[mars0i]

OK--reaching out to friends ....

[Dean Young]

do you think the project could incorporate 

• Principal bundle theory
• Connections
• The De Rham homomorphism

[Joseph Tooby-Smith]

Hey @Dean Young !

Yes I do. With the caveat that Mathlib seems a better place for the general theory behind these things. However, all or part of the general theory can also sit in HepLean until ready to go into Mathlib.

We will certainly want specific manifestations of these in HepLean, and properties of these specific manifestations. Principal bundles and connections would be useful now, and there are certain directions people could go in which will make De Rham cohomology etc useful. (Topological terms is an example).

[Joseph Tooby-Smith]

I have the first implementation of informal definitions and informal lemmas and their display here: https://heplean.github.io/HepLean/Informal.html. Going forward I plan to:

1. Make them more detailed, giving a 'roadmap' style thing.
2. Display them as a dependency graph. (update: Now done here)

[Tyler Josephson ⚛️]

mars0i said:

Joseph Tooby-Smith, for whatever it's worth, I think that there may be some philosophers of physics who might be very interested in this project and its goals. Not necessarily to help with proofs, but maybe that too. They might just be interested in paying attention to what's being done in this project. My area is philosophy of biology, but if you think it might be worthwhile, I would ask around with philosophers of physics.

If you or any of your colleagues are curious about my work in formalizing chemistry, let me know, I'd love to chat!

[mars0i]

Thanks @Tyler Josephson ⚛️. Cool. There are many philosophers of physics, but few philosophers of chemistry--and odd fact about philosophy of science. However, I think some of the philosophers of physics may be interested, so I'll try to pass it on. (Personally, I am curious but given my fairly shallow knowledge of chemistry, I don't think I'll pursue it further at present.)

[Tyler Josephson ⚛️]

@mars0i I found this journal just this week - looks like an interesting community. I'm an amateur philosopher, myself, but a professional chemical engineer; I've certainly never had formal philosophical training (nor do I write humanities-style articles), but I think bringing formal logic into chemistry requires a philosophical perspective that most engineers don't have.

[mars0i]

Ah, very nice @Tyler Josephson ⚛️. I didn't know about that journal. Maybe there's a lot more work in philosophy of chemistry than I knew about.