  Logicians at the R\'enyi Mathematical Institute in Budapest have spent
several years developing versions of relativity theory (special, general, and
other variants) based wholly on first order logic, and have argued in favour of
the physical decidability, via exploitation of cosmological phenomena, of
formally undecidable questions such as the Halting Problem and the consistency
of set theory.
  The Hungarian theories are very extensive, and their associated proofs are
intuitively very satisfying, but this brings its own risks since intuition can
sometimes be misleading. As part of a joint project, researchers at Sheffield
have recently started generating rigorous machine-verified versions of the
Hungarian proofs, so as to demonstrate the soundness of their work. In this
paper, we explain the background to the project and demonstrate an Isabelle
proof of the theorem "No inertial observer can travel faster than light".
  This approach to physical theories and physical computability has several
pay-offs: (a) we can be certain our intuition hasn't led us astray (or if it
has, we can identify where this has happened); (b) we can identify which axioms
are specifically required in the proof of each theorem and to what extent those
axioms can be weakened (the fewer assumptions we make up-front, the stronger
the results); and (c) we can identify whether new formal proof techniques and
tactics are needed when tackling physical as opposed to mathematical theories.
