Skip to content

mathematics

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:

    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.

      Special Issue on Mathematics in Artificial Intelligence

        Paola Galdi and Jacques Fleuriot are editing a special issue of the journal Mathematics in Computer Science focused on the interplay between mathematics and AI. The Call for Papers can be found here. The submission deadline is on the 31st of January 2024.