A project involving Carlin MacKenzie, James Vaughan and Jacques Fleuriot has resulted in a re-design and re-implementation of the Archive of Formal Proofs, which is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. The revamped website (https://www.isa-afp.org) is now live and will serve the Isabelle community across the world. The Edinburgh team worked with Fabian Huch of TU Munich to integrate their work into the AFP infrastructure.
Our formalisation of Schutz’ Independent Axioms for Minkowski Spacetime is now available in Isabelle’s Archive of Formal Proof. More information and the theories are available here.