physics

Stream: maths

[Juho Kupiainen]

Is someone by any change formalizing (formalized) physics math in Lean?

[Patrick Massot]

I don't think so (unless calculus and linear algebra count as physics).

[Bryan Gin-ge Chen]

There was this thread by @Kevin Sullivan. I think the corresponding repository is here. This thread is also related to that project.

[Jesse Michael Han]

I think at some point, @Michael R Douglas was considering formalizing quantum field theories in Lean.

[Michael R Douglas]

I am interested in it but there are many many prerequisites to do first.
Before working on QM and QFT we need basic functional analysis and especially Fourier analysis.
Another prerequisite of very broad relevance to physics and math is the theory of Lie algebras and Lie groups.
I started working on this with Anthony Bordg, we are doing it in Isabelle to use smooth manifolds as defined by Immler and Zhan.
Even this needs a good amount of additional material to get anywhere.

Here is my suggestion for a project with very very broad relevance: make a general definition of a hypersurface in R^n or C^n.
In other words one is given a function f:R^n\rightarrow R such that f=0 => grad f \ne 0, and the goal is to define the set of solutions of f(x)=0 as a smooth manifold with its maximal chart. This would enable us to define a huge list of manifolds including the most important Lie groups and homogeneous spaces in one shot!