Wed 18 October 2017: Assia Mahboubi (Inria and U Nantes), Room P-647, 16:00-17:00
Title: Machine-checked proofs
Abstract: Proof assistants belong to the large collection of tools available today for "doing mathematics with a computer". These systems allow their users to check with the highest degree of certainty the validity of the proofs they have carefully described to the machine. Formalized mathematics refers to the digitized mathematical data (definitions, theorems, and proofs) amenable to computer processing, and checking. Formalized mathematics provides a very high correctness guarantee, and can be used to verify proofs based on large-scale
computations. But it can also lead to the discovery of new constructions and proofs, and helps to organize mathematical knowledge with the help of a computer. In this talk, we will give a glimpse of the variety of research areas and methodologies involved in the area of machine-checked proofs, from the meta-mathematical properties of the underlying logical language, to the design and features of the proof assistant. We will try to illustrate what formalizing mathematics looks like on the concrete example of the formal verification of a
computer-algebra based proof of the irrationality of ζ(3). The latter example is a joint work with Frédéric Chyzak (Inria) and Thomas Sibut-Pinote (Microsoft Research).
Wed 01 November 2017: Henk Don (RU), Room P-647, 16:00-17:00
Wed 15 November 2017: Eddie Nijholt (VU), Room P-647, 16:00-17:00
Wed 29 November 2017: Rikkert Hindriks (VU), Room P-647, 16:00-17:00
Wed 13 December 2017: Wouter Hetebrij (VU), Room P-647, 16:00-16:15
Wed 13 December 2017: Joey van Langen (VU), Room P-647, 16:20-16:35
Wed 13 December 2017: Jaap Storm (VU), Room P-647, 16:45-17:00
Previous talks in 2017:
Wed 04 October 2017: Wadim Zudilin (RU), Room P-647, 16:00-17:00
Title: Variations on One over Pi
Abstract: The number $\pi=3.1415926\dots$ is recognised as the bestselling mathematical constant of all the time. One hundred years ago, well before the era of the computer, the Indian prodigy Srinivasa Ramanujan found a remarkable list of formulae for $1/\pi$, which can be used to compute the quantity to several thousand places. Today, Ramanujan's equations are still in use. The last few decades have witnessed an exploding development of new methods and generalisations of these formulae, bringing together topics from analysis, combinatorics, algebraic geometry, differential equations and number theory. At the same time, we lack understanding about the structure of such generalisations. In my talk, I will surf on the waves of the story of $1/\pi$.
Wed 20 September 2017: Rob van der Mei and Martin van Buuren (VU), Room P-647, 16:00-16:30
Title: Applied Mathematics in Practice: How to Save Lives with Maths?
Abstract: In this talk, we will talk about (1) stochastic models for how to reduce emergency response times by smart proactive relocations of ambulance vehicles, and (2) how these models work in real-life.
Wed 17 Mei 2017: Elenna Dugundji, Room P-647, 16:00-17:00
Title: Social and spatial interactions in transportation mode choice.
Abstract: To what extent are consumers influenced in their choice of mode of transport by their neighbors’ choices? Or the choices made by peers in their social circle? These are important questions to understand for both policy makers and private sector parties interested in promoting particular modes of transport, but they have only recently attracted attention of transportation researchers. We discuss a socio-dynamic variant of a classic approach to predictions in this context, from both theoretical and empirical points of view, including an application to mobility in Amsterdam.
Wed 03 Mei 2017: Bernard Zweers, Room P-647, 16:00-16:15
Title: Minimizing the cost for inland container transportation
Abstract: A real-life operational planning problem for a logistic service provider is considered. A number of containers have to be shipped from multiple deep sea terminals to a single inland terminal. On may choose the day of transportation and the mode: truck or barge. The goal is to find an assignment for the containers that minimizes the total costs without visiting too many terminals with one barge. For this purpose an integer linear program is formulated that can solve practical instances in reasonable time.
Wed 03 Mei 2017: Jan-David Salchow, Room P-647, 16:20-16:35
Title: Function spaces on manifolds
Abstract: The foundation for existence and regularity of solution spaces of PDE is the theory of function spaces. While historically most interest was directed towards PDE on subspaces of R^n, there is a growing demand for function spaces on Riemannian manifolds. In my talk
I will report on recent progress in the theory of Sobolev spaces on manifolds.
Wed 03 Mei 2017: Chris Groothedde, Room P-647, 16:40-16:55
Title: Instability in Dynamical Systems with Delayed Feedback
Abstract: Many mathematical models describe systems with feedback loops. When this feedback is not instantaneous the behaviour and analysis of such a system becomes much more complex. In this talk we will look at equilibrium solutions of such Delay Dynamical systems and the instability that occurs near equilibrium solutions. The set of unstable solutions originating in an equilibrium can be described as a manifold: the Unstable manifold. In particular I will explain some of the basic functional analytic setup behind the study of Delay Dynamical Systems and their Equilibria and how to describe and visualise the Unstable Manifolds.
Wed 19 April 2017: Mark Veraar (TUD), Room P-647, 16:00-17:00
Title: Fourier multiplier theory: old and new results
Abstract: Using Fourier multiplier theory one can prove the L^p-boundedness of many singular integrals. The first Fourier multipliers theorem has been proved by Marcinkiewicz in 1939. His main motivation was the application to elliptic PDEs. Since his work there have been many results on multiplier theory, among which the results of Mihlin and H\"ormander. During the last 20 years, multiplier theory was extensively studied in the weighted setting and in the vector-valued setting. The weighted setting is motivated by complex and geometric analysis and has led to several famous results. The vector-valued setting is important in the operator theoretic approach to PDE. In the talk I will present a survey of some of the recent results and their applications
Wed 05 April 2017: Sandjai Bhulai (VU), Room P-647, 16:00-17:00
Title: Value Function Discovery In Markov Decision Processes.
Abstract: In this talk, we introduce a novel method for discovery of value functions for Markov Decision Processes (MDPs). This method is based on ideas from the evolutionary algorithm field. Its key feature is that it discovers descriptions of value functions that are algebraic in nature. This feature is unique, because the descriptions include the model parameters of the MDP. The algebraic expression can be used in several scenarios, e.g., conversion to a policy, control of systems with time-varying parameters. We illustrate its application on an example MDP.
Wed 22 Maart 2017: Bart de Smit (RUL), Room P-647, 16:00-17:00
Title: On the abelian coverings of curves over finite fields.
Abstract: The main result of this talk identifies when two curves over finite fields have equivalent categories of (possibly ramified) abelian coverings. We will also sketch where this result fits in the wider context of number theoretic analogs of Kac's famous question: "Can you hear the shape of a drum?".
Wed 08 Maart 2017: Daan Crommelin (UvA and CWI), Room P-647, 16:00-17:00
Title: Stochastic models for multiscale dynamical systems
Abstract: Modeling and simulation of multiscale dynamical systems such as the climate system is challenging due to the wide range of spatiotemporal scales that need to be taken into account. A promising avenue to tackle this multiscale challenge is to use stochastic methods to represent dynamical processes at the small/fast scales. The feedback from microscopic (small-scale) processes is represented by a network of Markov processes conditioned on macroscopic model variables. I will discuss some of the work from this research direction. A systematic derivation of appropriate stochastic processes from first principles is often difficult, and statistical inference from suitable datasets can provide an interesting alternative.
Wed 22 Februari 2017: Jens Rademacher (Bremen), Room P-647, 16:00-17:00
Title: Nonlinear waves: gems in evolution equations.
Abstract: While the overall dynamics of an evolution equation can be complicated and even inaccessible to an analysis, there are often subsystems that allow for more. A prominent case are nonlinear waves in parabolic partial differential equations with an extended spatial direction. The simplest such solutions have constant shape up to translation. Examples are solitons, excitation waves and periodic patterns. The identification of such objects is not only much easier than the task to understand the dynamics of the overall problem. These nonlinear waves often form building blocks for more complex behaviour, and, last but not least, often shape the phenomena that are of most interest in applications. In this talk some prominent examples will be present, combined with a brief introduction to analytic tools for existence and stability analysis.
Wed 08 Februari 2017: Richard J. Boucherie (Twente), Room P-647, 16:00-17:00
Title: Operations research solutions to improve the quality of healthcare
Abstract: Healthcare expenditures are increasing in many countries. Delivering adequate quality of healthcare requires efficient utilization of resources. Operations Research allows us to maintain or increase the current quality of healthcare for a growing number of patients without increasing the required work force. In this talk, I will describe a series of mathematical results obtained in the Center for Healthcare Operations Improvement and Research of the University of Twente, and I will indicate how these results were implemented in Dutch hospitals.
Efficient planning of operating theatres will reduce the wasted hours of staff, balancing the number of patients in wards will reduce peaks and therefore increases the efficiency of nursing care, efficient rostering of staff allows for more work to be done by the same number of people. While employing operations research techniques seems to be dedicated to improving efficiency, at the same time improved efficiency leads to increased job satisfaction as experienced workload is often dominated by those moments at which the work pressure is very high, and it also improves patient safety since errors due to peak work load will be avoided.