GR, Yang-Mills, and manifolds

Stream: Natural sciences

[Winston Yin (尹維晨)]

General relativity and QFT seem to be areas in which there’s a need for a high level of mathematics beyond mere computation. If not useful to physicists at large, they could at least generate some interest from the mathematical physics crowd to pay attention to formalisation.

GR is an obvious motivation to develop the theory of (pseudo-)Riemannian manifolds. One tangible target there could be the statement of Einstein’s field equations and proofs that certain spaces are solutions to them. The development of mathlib in this direction could lead to Ricci flows, which are central to the proof of the Poincaré conjecture, the only millennium prize problem to be solved thus far.

In QFT, a gauge theory can be interpreted as an equation on the connection of a fibre bundle where the fibres are some Lie group. The connection would then be a section on the vector bundle where the fibre is the corresponding Lie algebra. One goal would be to classify topological defects such as monopoles, instantons, and strings. Development in this direction would lead to the correspondence between Lie groups and Lie algebras, the classification of semisimple complex Lie algebras, and de Rham cohomology.

There are of course many other topics, but I’m mentioning these because there’s recently been a very nice refactor of the fibre bundle API on mathlib, and I’ve been working (very slowly) on formalising the exponential map on Lie groups. If we can get the more mathematically inclined physicists on board, mathlib will become much more diverse in content (that is still relevant in mathematics proper).

Let me know if you’re interested in getting involved!

[Winston Yin (尹維晨)]

(deleted)

[Marcello Seri]

I'd be interested on the manifold side for hamiltonian systems, and symplectic and poisson geometry

[Joseph Tooby-Smith]

I used to be a particle phenomenologist, then a formal high energy theorist and now someone who codes in lean… (don’t ask how the job hunt is going :P).


Here is a vision of what I think would be good: A library like (and dependent on) Mathlib for high energy physics (inc. GR). The library should contain both definitions and proofs of important theorems and lemmas. It should also contain the formal verifications of calculations such as “the cross section of... is…”, “this potential has a phase transition at …”. Basically everything in HEP that doesn’t require experimental data. It should be well-documented and the long term goal should be to make it actually useful for physicists.

If we can get another people that are eager to help with something like this, it would be great.

[Tyler Josephson ⚛️]

Do you have any recommended sources on formalized or non-formalized versions of these? I teach Lean to undergrads in science and engineering, and if I find an interested student, could see if they want to work on it.

[Winston Yin (尹維晨)]

I feel that there’s still a lot of foundational work to be done. For example, we should first have a library of common differential equations and solutions. On the GR side, mathlib doesn’t have (pseudo)Riemannian manifolds yet, but people have written working definitions. There needs to be something akin to the Xena project but for physics, aiming to formalise the undergraduate physics curriculum.

[Winston Yin (尹維晨)]

@Tyler Josephson ⚛️ What’s your experience teaching Lean to science and engineering students? What is your goal, and what are some challenges you’ve met?

[Joseph Tooby-Smith]

@Winston Yin (尹維晨) I suggested something along the lines of what you are suggesting for undergraduate physics at:

https://leanprover.zulipchat.com/#narrow/stream/395462-Natural-sciences/topic/Undergraduate.20Physics/near/393069237

I actually no longer think this is necessarly best way forward. For two reasons: Firstly, there will be some areas of physics which are much harder to formalize than others. Secondly, I'm not sure it would convince any physicist that doing things in lean is a good idea.

I think one should imagine giving a talk to a bunch of research-level physicists about lean. The first thing they are likely going to ask is "why should I care about this, and how does it help me?". I think a project which starts with coming up with a convincing answer to this question with explicit examples is much more likely to get traction than formalizing undergraduate physics - which can come later.

[Tyler Josephson ⚛️]

@Winston Yin (尹維晨) I've had ~10 non-CS / math undergraduates learn or try learning Lean, with 3 so far who picked up enough to make significant contributions in proofs and/or programming. All of them were able to essentially self-teach from the online textbooks, but not everyone can do this.

Last summer, I led an 8-week meeting series on "Lean for Scientists and Engineers." We mostly followed @Heather Macbeth's Mechanics of Proof. This is an excellent resource for science and engineering students, since it only assumes sophomore-level math.

[Tyler Josephson ⚛️]

We don't have curriculum tailored to the needs of science and engineering students, and I'm working on this. When we reprise "Lean for Scientists and Engineers" this summer, we'll combine parts from Mechanics of Proof, Mathematics in Lean, and Functional Programming in Lean, and add example exercises and problems from physics, chemistry, and engineering.

The plan at the moment (subject to change as I develop things and reflect) is to cover installation and basics of Lean, then have 3 modules: proofs, programs, and proofs about programs (the first two may be sequential or somewhat parallel, we'll see). "Proofs" will do basics of tactics and calc blocks for equalities/inequalities, then drive towards calculus based proofs by doing sets --> topology --> differential calculus --> integral calculus. "Programs" will cover the type system, structures, running programs, and input/output, and will show Lean code alongside identical examples as Python and MATLAB versions (to help those with prior programming experience). Then "proofs about programs" will discuss the halting problem as taught here, then dig into polymorphic functions (our most promising strategy for real/float translation, at the moment) that enable proofs to be written real-valued functions that can also execute floating point calculations (active research by @John Velkey ⚛️ and @Tomas Skrivan).

Reasons for this structure are:
1) Most physics / chemistry derivations worth doing require calculus. I'm trying to figure out the shortest path to calculus for students who haven't yet taken a logic course. Will be consulting with math educators for opinions on this once I start nailing down the content.
2) "Bug-free simulations" is how I motivate my group's investment in Lean, and I think this will have traction among other scientists and engineers, too. But proofs alone don't show this, we need functions that can be executed in a simulation / regression context, to ground things in the real world, and these can't be limited to natural numbers. I dream of a solution to the real/float translation issue that can accommodate a simple #eval-like command that simply handles real/rational inputs as floats; maybe we'll have a version of this with polymorphic functions by this summer.

[Tyler Josephson ⚛️]

Joseph Tooby-Smith said:

Winston Yin (尹維晨) I suggested something along the lines of what you are suggesting for undergraduate physics at:

https://leanprover.zulipchat.com/#narrow/stream/395462-Natural-sciences/topic/Undergraduate.20Physics/near/393069237

I actually no longer think this is necessarly best way forward. For two reasons: Firstly, there will be some areas of physics which are much harder to formalize than others. Secondly, I'm not sure it would convince any physicist that doing things in lean is a good idea.

I think one should imagine giving a talk to a bunch of research-level physicists about lean. The first thing they are likely going to ask is "why should I care about this, and how does it help me?". I think a project which starts with coming up with a convincing answer to this question with explicit examples is much more likely to get traction than formalizing undergraduate physics - which can come later.

I'll be giving a talk to the Materials Genome Initiative at NIST at the end of the month, pitching my group's efforts formalizing chemical physics in Lean to write bug-free software. I don't have many connections to physicists, but would be happy to speak if invited.

[Joseph Tooby-Smith]

@Tyler Josephson ⚛️ I just had a brief scan through your paper. It looks really good. The sorts of theorems and definitions you have there are the sorts of things I would want in library for e.g. high energy physics.

I think motivation of providing "bug-free software" is a great one! Maybe it wouldn't convince the pen-and-paper physicist (like myself), but we are in the minority. For the pen-and-paper physicist, I think the motivation has to come from the checking of computations, and proofs, and perhaps the `ease' of using lean over doing things by hand.