Skip to content

Isabelle

Reconstruction of Euler’s proof published in the AFP

    Our development of “Euler’s Exponential Series as an Infinite Polynomial” has been accepted and published by the Archive of Formal Proofs.

    Abstract:
    In this formalisation, we reconstruct Euler’s derivation of the power series for the exponential function as expounded in his famous Introductio in analysin infinitorum, first published in 1748. Using nonstandard analysis, we mechanize his mixture of infinitesimal and infinite ‘algebraic’ reasoning in the proof assistant Isabelle. In so doing, we demonstrate that the gist of his arguments can be reconstructed formally, with Isabelle and nonstandard analysis shoring up crucial aspects of his reasoning that some historians have qualified as being “more a matter of faith than science”.

    The full formalization is available here:

    IsaGrad paper accepted at LogicNN 2026

      Our paper “IsaGrad: Verified Automatic Differentiation over Computational Graphs in Imperative HOL” has been accepted and will be presented at LogicNN, FLOC 2026.

      The Gelfand–Naimark–Segal Construction published in the AFP

        Our development of the “The Gelfand–Naimark–Segal Construction” has been accepted and published by the AFP.

        Abstract

        This entry formalises complete normed algebras equipped with an involution, so-called C*-algebras. We provide both a class definition, and a locale for C*-algebras on carrier sets in the spirit of existing developments of linear algebra and smooth manifolds. Bounded operators on a complex Hilbert space, with the operator norm and adjoints, form such an algebra. The main theorem of this entry is a result in the converse direction: the Gelfand–Naimark–Segal (GNS) construction, which starts with a single suitable functional on a C*-algebra in order to obtain both a Hilbert space and a representation of the algebra in terms of bounded operators on that space. This is implemented as a type construction in Isabelle/HOL, taking advantage of existing mechanisms for quotient types, and integrating with existing type classes for Hilbert spaces and Cauchy completions.

        The full formalisation is available here.

        Our paper on differentiable Signal Temporal Logic for neurosymbolic AI has been published by LIPIcs

          GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning

          Authors Mark Chevallier , Filip Smola , Richard Schmoetten , Jacques D. Fleuriot 

          Part of: Volume: 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)
          Series: Leibniz International Proceedings in Informatics (LIPIcs)
          Conference: International Symposium on Temporal Representation and Reasoning (TIME)

          Our preprint on formally verified neurosymbolic trajectory learning is out on arXiv

            Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces

            Astract:

            We present a novel formalisation of tensor semantics for linear temporal logic on finite traces (LTLf), with formal proofs of correctness carried out in the theorem prover Isabelle/HOL. We demonstrate that this formalisation can be integrated into a neurosymbolic learning process by defining and verifying a differentiable loss function for the LTLf constraints, and automatically generating an implementation that integrates with PyTorch. We show that, by using this loss, the process learns to satisfy pre-specified logical constraints. Our approach offers a fully rigorous framework for constrained training, eliminating many of the inherent risks of ad-hoc, manual implementations of logical aspects directly in an “unsafe” programming language such as Python, while retaining efficiency in implementation.

            Paper: https://arxiv.org/abs/2501.13712

            Our formalisation of Linear Resources and Process Compositions has been published in the Archive of Formal Proof

              Abstract

              In this entry we formalise a framework for process composition based on actions that are specified by their input and output resources. We verify their correctness by translating compositions of process into deductions of intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction.

              We describe an earlier version of this formalisation in our article Linear Resources in Isabelle/HOL, which also includes a formalisation of manufacturing processes in the simulation game Factorio.

              Our formalisation of Lie Groups and Algebras has been published in the Archive of Formal Proof

                Abstract

                Lie Groups are formalised as locales, building on the AFP theory of Smooth Manifolds. We formalise the diffeomorphism group of a manifold, and the action of a Lie group on a manifold. The general linear group is shown to be a Lie group by proving properties of the determinant, and matrix inverses. We also develop a theory of smooth vector fields on a manifold , defined as smooth maps from the manifold to its tangent bundle . We employ a shortcut that avoids difficulties in defining the tangent bundle as a manifold, but which still leads to vector fields with the properties one would expect. We then construct the Lie algebra of a Lie group as an algebra of left-invariant smooth vector fields.

                Schmoetten R. and Fleuriot J. D. (2024). Lie Groups and Algebras. Archive of Formal Proofs. ISSN: 2150-914x.

                Our paper “Linear Resources in Isabelle/HOL” has just been published in the Journal of Automated Reasoning

                  Abstract:

                  We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of these compositions is verified by translating them into deductions in intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction when satisfied. We mechanise the whole framework, including a deep embedding of ILL, in the proof assistant Isabelle/HOL. Beyond the increased confidence in our proofs, this allows us to automatically generate executable code for our verified definitions. We demonstrate our approach by formalising part of the simulation game Factorio and modelling a manufacturing process in it. Our framework guarantees that this model is free of bottlenecks.

                  Smola, F., Fleuriot, J.D. Linear Resources in Isabelle/HOL. J Autom Reasoning 68, 9 (2024). https://doi.org/10.1007/s10817-024-09698-2

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