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

[Mark Ettinger]

I've formalized all the concepts necessary to prove (with help from Harmonic's Aristotle) that an inertial observer always moves strictly slower than the speed of light relative to another initial observer. Here is the the repo if anyone is interested: https://github.com/mettinger/Relativity

This raises a couple of questions for me:

1. Is this material appropriate for any library? It seems tangential to mathlib I think. I'm not sure if I'll take the project further if it remains a strictly personal exercise.

2. I used Lean 4.24 for compatibility with Aristotle. There seem to be a surprising number of incompatibilities with the current version (4.28). Is it common for new versions of Lean and/or mathlib to break proofs or am I making some sort of mistake?

[James E Hanson]

Mark Ettinger said:

Is it common for new versions of Lean and/or mathlib to break proofs or am I making some sort of mistake?

I believe this is common for proofs that are not written with 'durability' in mind. For instance, this is why people say you should avoid non-terminal simps.

[Weiyi Wang]

As some data points, my project of a few thousands of lines typically experiences 1 to 5 minor breaks (takes 10 minutes to fix) when upgrading for each version. I wrote proofs with durability in mind

[Joseph Tooby-Smith]

1. Is this material appropriate for any library? It seems tangential to mathlib I think. I'm not sure if I'll take the project further if it remains a strictly personal exercise.

In theory it is subtle for PhysLean, and it would be great to have this, but may require some work to integrate it properly.