Skip to content

theorem proving

Paper accepted at CICM 2022

    Our paper, “Re-imagining the Isabelle Archive of Formal Proofs” (MacKenzie, Huch, Vaughan and Fleuriot), has been accepted at the 15th Conference on Intelligent Computer Mathematics (CICM 2022).

    New Archive of Formal Proof Website

      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 ( 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.

      Mark Chevallier passes his second year PhD review

        Mark successfully passed his second year PhD  review on formal verification applied to machine learning. His panel consisted of Pavlos Andreadis, Paul Jackson and Jacques Fleuriot. Congratulations to Mark!