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)