Skip to content

Talks

Exploring Euler’s Differentials of Exponential Functions in Isabelle using Nonstandard Analysis

    Date: 16th October 2020
    Time: 00:00 - 00:00

    Title: Exploring Euler's Differentials of Exponential Functions in Isabelle using Nonstandard Analysis
    Speaker: Richard Stansfield
    Abstract:

    Many of the proofs of important results in analysis from Euler’s Foundations of Differential Calculus have been called into question due to their lack of rigour and reliance on the existence of infinitely small numbers, which standard mathematics now rejects. However, using nonstandard analysis formalised in Isabelle we may now be able to rigorously rehabilitate them and in doing so uncover the implicit reasoning behind some of the legendary mathematician’s results.

    In particular, my project will focus on a handful of proofs regarding differentials of functions involving exponentiation. I will talk about the background to the project – hopefully giving an intuitive impression of nonstandard analysis for the unfamiliar – as well as discussing some of the difficulties that arise when converting Euler to Isabelle.

    Exploring Euler’s Differentials of Trigonometric Functions in Isabelle using Nonstandard Analysis

      Date: 16th October 2020
      Time: 14:00 - 16:00

      Title: Exploring Euler's Differentials of Trigonometric Functions in Isabelle using Nonstandard Analysis
      Speaker: Alice Johansen
      Abstract:

      In 1755, Euler published his influential 'Foundations of Differential Calculus' which presented and defined theories of differential calculus and discussion of the infinite. While Euler makes missteps and often excludes assumptions in his proofs, one must remember that in context, eighteenth-century mathematicians did not have the same expectations of rigour that one might have today, and thus there is value in formulating Euler’s reasoning now with the diligence that his text lacked. Returning to our current time, interactive proof assistant Isabelle has helped verify countless theorems across mathematics and computer science domains, and I will use this powerful tool to explore and prove Euler's differential definitions for trigonometric functions sin, cos and hopefully more via nonstandard analysis

      Detection of the Time Required to Find a Study Space in the UoE Main Library using Wi-Fi Data

        Date: 16th October 2020
        Time: 14:00 - 16:00

        Title: Detection of the time required to find study space in the Main Library using Wi-Fi data
        Speaker: Dimitris Christodoulou
        Abstract:

        Finding empty space to study in the Main Library can be challenging, particularly in busy periods such as during exams. The aim of this project is to analyse WiFi data in an effort to detect movement patterns in the Library and identify users that eventually settle down in a particular study space. This data will then be used to provide indications or predictions of how long it may take to find an empty study space at any given time.

        Automated HOL Light Theorem Annotation

          Date: 16th October 2020
          Time: 14:00 - 16:00

          Title: Automated HOL Light Theorem Annotation
          Speaker: Timmy Gill
          Abstract:

          This talk will introduce my work looking to find ways to tag theorems in HOL Light corpora with their associated areas of mathematics. It is hoped that this will enhance users' ability to understand theorems, quickly find groups of related theorems and more easily navigate libraries to find relevant lemmas for proofs. I will introduce some of the methods I propose to use to generate/ propagate tags and
          describe the intuition for using them in this context.

          Looking Ahead in Discrete Event Simulation

            Date: 2nd October 2020
            Time: 14:00 - 16:00

            Title: Looking Ahead in Discrete Event Simulation
            Speaker: Michal Baczun
            Abstract:

            Discrete event simulation is a common method for analysing business processes for the purposes of predictive analytics, optimisation, and exploring possible “what-if” scenarios. Modelling a process and its environment with the appropriate level of detail for the purposes of the simulation can be challenging, and often simulations cannot support certain features of a process. One such example is the prioritisation of tasks, and scheduling that considers the priorities of not only current but also future tasks. In this presentation I will discuss the value of look-ahead functionality in workflow simulation, and how we have incorporated look-ahead capabilities into an existing discrete event simulation environment, namely WorkflowFM.

            Formalisations of Q learning and logic as a loss function

              Date: 2nd September 2020
              Time: 14:00 - 16:00

              Title: Formalisations of Q learning and logic as a loss function
              Speaker: Mark Chevallier
              Abstract:

              Q learning is a form of reinforcement learning where we try to learn how to navigate through an environment where we can earn rewards by earning the biggest reward possible.

              I have been working on its formalisation in the theorem prover Isabelle/HOL, and in this talk I will give details about the different ways I have tried to represent rewards and value, and the pitfalls I have discovered making progress along the way.

              I will also be discussing a formalisation of a method of evaluating logical constraints as real numbers to use them as part of a loss function in a neural network. This method has been described by others, and by formalising their methods I uncovered a lack of rigour and a better way to approach some of the issues that arose.

              I will demonstrate that I was able to use Isabelle/HOL to generate working code based on my formalisation to guarantee the code fulfils the specifications exactly and eliminate any possibility of human error in implementation.

              Towards a mechanisation of Euler’s Infinite Analysis in the Proof Assistant Isabelle

                Date: 31st August 2020
                Time: 14:00 - 16:00

                Title: Towards a mechanisation of Euler's Infinite Analysis in the Proof Assistant Isabelle
                Speaker: Imogen Morris
                Abstract: 

                In 1736 Euler published a proof of an astounding relation between π and the reciprocals of the squares.

                π ² ⁄ 6 = 1+ 1⁄4 + 1/9 + 1/25 + ...

                Until this point, π had not been part of any mathematical relation outside of geometry. This relation would have had an almost supernatural significance to the mathematicians of the time. But even more amazing is Euler's proof. He factorises a transcendental function as if it were a polynomial of infinite degree. He discards infinitely-many infinitely-small numbers. He substitutes 1 for the ratio of two distinct infinite numbers.

                Nowadays Euler's proof is held up as an example of both genius intuition and flagrantly unrigorous method. In my talk I will describe how, with the aid of nonstandard analysis, which gives a consistent formal theory of infinitely-small and large numbers, and the proof assistant Isabelle, we are in the process of constructing a formal proof of the Basel problem which uses the method of Euler's original proof. We argue that Euler was consistent in his use of infinitely-large and infinitely-small numbers, and aim to show that his original reasoning provides the structure of a formal proof. We use the concept of "hidden lemmas", developed by McKinzie and Tuckey based on Lakatos and  Laugwitz, to formalise general principles which Euler's proof followed. Towards this end, we have developed a theory of infinite "hyperpolynomials", formal proofs of a version of convergence of the infinite polynomials used by Euler, formalisation of the factorisation and expansion of Euler's infinite polynomial and formal proofs of many steps in Euler's proof.

                This talk is part of my 3rd year review and will describe my work done so far, as well as the planned work, which together will become my PhD thesis.

                Creating a framework for comparing and selecting process discovery algorithms

                  Date: 16th July 2020
                  Time: 14:00 - 16:00

                  Title: Creating a framework for comparing and selecting process discovery algorithms
                  Speaker: Demetris Louca
                  Abstract: Process discovery is the part of Process mining that creates a model to describe the behaviour of an event-log. Whether it is for training future doctors or optimising business processes, finding the underlying model is essential in gaining an understanding of the occurring processes.

                  There have been multiple algorithms proposed, such as the alpha-miner, heuristic miner, and others. However, there has not been enough work comparing the algorithms or linking their performance to the properties of the data.

                  This talk aims to outline the main algorithms in process discovery. Then, the overall performance of the algorithms will be compared experimentally by using a varied set of artificial data. But the overall performance of the generated models is linked to the data used, thus the talk aims to associate some of the descriptive statistics of the data-sets to the performance of algorithms.

                  Process Analytics for the Training of Future Doctors

                    Date: 16th July 2020
                    Time: 14:00 - 16:00

                    Title: Process Analytics for the Training of Future Doctors
                    Speaker: Yannan Huang
                    Abstract: Process Mining is an emerging discipline which is used to deal with process data: event log (the record of execution) and process model. Given the log of future doctor training and the referenced process model, this project is mainly split into two parts: the first part is an analytical methodology and a corresponding report for students and instructors. The second part is an automatic scoring framework for the training process using conformance checking techniques in process mining: Token-based and Alignment Conformance Checking. Besides, the performance of techniques, such as robustness, will be evaluated and compared.

                    Formalising Minkowski Spacetime

                      Date: 3rd July 2020
                      Time: 14:00 - 16:00

                      Title: Formalising Minkowski Spacetime
                      Speaker: Richard Schmoetten
                      Abstract: My MSc project proposes to formalise an axiomatic system for Minkowski spacetime in the proof assistant Isabelle. I will outline the axioms as originally published by John Schutz in 1997, contrasting them with our current formalisation in Isar. The procedure of de-sugaring and converting a prosaic definition to a workable Isabelle/Isar object is illustrated with an example central to many of the results we are interested in. Using some of our proofs (finished and otherwise) as examples, I will expand on the difficulties I have encountered so far as a novice to automated reasoning.