Skip to content

Talks

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.

          Building an Interpretable Classifier for Brain Tumour Prediction

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

            Title: Building an Interpretable Classifier for Brain Tumour Prediction
            Speaker: Colleen Charlton
            Abstract: Patients with a brain tumour may present with general non-specific symptoms that vary depending on the location and size of the tumour. Thus diagnosis of a brain tumour is difficult, which is compounded by the rarity of the condition.  My project aims to build an interpretable rule-based machine learning model using a UK dataset that can assess a patient’s likelihood of a brain tumour based on their presenting symptoms.  The final interpretable model may act as a second opinion to assist general practitioners in patient referral and diagnosis.

             

            Applying Process Mining to Healthcare Data for Use with DataLoch

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

              Title: Applying Process Mining to Healthcare Data for Use with DataLoch
              Speaker: Anita Klementiev
              Abstract: 

              Process mining is a set of techniques for extracting knowledge about processes from timestamped event log data. When applied to hospital information system (HIS) data, process mining can be used to find the most frequently followed patient care paths, investigate differences in care paths followed by different patient groups, analyse compliance with internal and external guidelines, and identify bottlenecks. This talk will give an overview of these different use-cases for process mining, along with a selection of case studies where process mining has been applied to HIS data. Additionally, this talk will cover my applications of process mining using the MIMIC III Intensive Care dataset and the resulting process models. Finally, I will discuss what kind of insights we hope to gain from this experimentation in order to inform meaningful use of process mining with the Edinburgh and South East Scotland data repository known as DataLoch, which is currently under development at the Usher Institute.

              Network Motifs – the Building Blocks of Networks

                Date: 5th June 2020
                Time: 14:00 - 16:00

                Title: Network Motifs - the Building Blocks of Networks
                Speaker: Valerio Restocchi
                Abstract: Networks are an exceptional way to describe a number of different complex systems, from viruses to social networks. The introduction of network motifs (i.e. small, repeating subgraphs) around 15 years ago, has opened up many new ways to look at the relational information embedded in networks, and started a new field of research. In this talk, I will give an overview of motifs, show some of the many interesting applications, and give some practical information about how to include them in (almost) any kind of research.

                The Suboptimal Principle of Optimality

                  Date: 24th April 2020
                  Time: 14:00 - 15:00

                  Title: The Suboptimal Principle of Optimality
                  Speaker: Mark Chevallier
                  Abstract: How proving the principle of optimality, within the context of reinforcement learning, has led to me rewriting how I calculate the Q value of a state-action twice in Isabelle - the original proof, intuitive and easy on paper, is much more difficult formally. I will also discuss my current approach to calculating Q values and how it should make proving the Principle of Optimality easier.

                  Formal Verification of Reinforcement Learning (Practice Talk)

                    Date: 13th March 2020
                    Time: 14:00 - 16:00

                    Title: Formal Verification of Reinforcement Learning (Practice Talk)
                    Speaker: Mark Chevallier
                    Abstract:

                    I will discuss my research into formal verification of discrete reinforcement learning, with particular emphasis on the possible benefits of this approach. This 10 minutes talk is intended for an audience familiar with reinforcement learning but perhaps not so familiar with formal verification or theorem proving.

                    Euler the Mathemagician (Take 2)

                      Date: 13th March 2020
                      Time: 14:00 - 16:00

                      Title:  Euler the Mathemagician
                      Speaker: Imogen Morris
                      Abstract:

                      I will give a practice talk for the 3 minute thesis competition. This will be a description of my PhD work on formalising Euler's use of the infinitely-small and large, but aimed at an intelligent lay-audience and designed to capture their interest and attention. I will do it as a complete dry-run this time e.g. remaining within 3 minutes and without notes. I would appreciate feedback on my delivery including but not limited to eye-contact, enthusiasm, use of gestures, speed, articulation and movement.