Special Relativity

Stream: Natural sciences

[Mark Ettinger]

Is there anyone here formalizing special relativity in Lean? I searched and found nothing so I assume not but I wanted to check. Here is an example of a brief introduction to an axiomatic approach to special relativity:

https://arxiv.org/abs/1005.0960

Here is a more extensive version, a preprint that eventually appeared in final form in "The Handbook of Spatial Logics":

https://old.renyi.hu/pub/algebraic-logic/Logicofspacetime.pdf

Here is a very preliminary formulation in Isabelle:

https://arxiv.org/abs/1211.6468

[Notification Bot]

A message was moved here from #Natural sciences > Physics in Lean by Mark Ettinger.

[Joseph Tooby-Smith]

There is some stuff in: https://github.com/HEPLean/HepLean
Currently it includes Lorentz vectors, tensors, Weyl fermions, the connection between the Lorentz group and SL(2,C) and I am working on an interface to do index notation.

This is all a start, and hopefully the project above eventually contain more aspects of special and general relativity. This also doesn't start from the axiomatic approach but by all means could.

[Tyler Josephson ⚛️]

Here’s another related reference, for formalizing in Coq: https://dash.harvard.edu/handle/1/38811518