Juho Kupiainen (Oct 17 2019 at 19:04):
Is someone by any change formalizing (formalized) physics math in Lean?
Patrick Massot (Oct 17 2019 at 19:05):
I don't think so (unless calculus and linear algebra count as physics).
Bryan Gin-ge Chen (Oct 17 2019 at 19:09):
Jesse Michael Han (Oct 19 2019 at 03:41):
I think at some point, @Michael R Douglas was considering formalizing quantum field theories in Lean.
Michael R Douglas (Oct 19 2019 at 16:48):
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!
Last updated: May 09 2021 at 11:09 UTC