Program

10:30 - 12:30 Scientific presentations (Conference room, IRMA)

Rodrigo IBATA (ObAS), "Our physics teacher, the Milky Way"
Abstract: Humanity is clearly at the beginning of a new technological and scientific revolution. In this talk, I will discuss our efforts to make machine learning explicable by uncovering the properties of dynamical systems in an objective manner, as well as by developing a new symbolic regression method for physics that searches for analytic laws that can represent simultaneously a variety of datasets.
These methodological efforts will be presented in the context of our work on exploring the dynamics and properties of the Milky Way with the Gaia space mission. In particular, I will discuss our recent work on trying to find stellar streams in our Galaxy, and trying to use them to reveal the properties of the dark matter.

Julien NARBOUX (ICube), "Proof assistants for teaching proof, motivations, and challenges"
Abstract: The terms proof assistant (PA), or interactive theorem prover (ITP), refer to a category of software tools designed to let a user interactively construct and verify the correctness of formal mathematical proofs. PAs such as Coq (ACM Software Award 2013), Isabelle, HOL-Light or Lean have been used successfully both to check proofs of mathematical properties (4 colors theorem, Hales’ theorem, Feit-Thompson’s theorem, Liquid Vector Spaces, …) and critical software (CompCert compiler - ACM Software Award 2021, SEL4 microkernel - ACM Software Award 2022,...).
PAs have been used for years in education in various contexts, for instance, to teach mathematical logic or elements of theoretical computer science. More recently, PAs have gained increased attention for teaching proof and proving. In this talk, I will give an overview of the different reasons why we think proof assistants may be useful in the classroom and list some of the previous experiments. I will present a joint work with Iro Bartzia, Emmanuel Beffara, and Antoine Meyer, where we emphasize how different proof assistants can impact student learning differently. I will report on our ongoing experiments in collaboration with Iro Bartzia and Pierre Boutry in the framework of the ANR project APPAM. We are currently experimenting with a proof assistant with a controlled natural language input language (Patrick Massot’s Lean-Verbose) and a proof assistant based on a point-and-click user interface (Frédéric Leroux’s Deaduction).

Rym SMAI (IRMA), "Enveloping space of a globally hyperbolic conformally flat spacetime"
Abstract: The physical theory of general relativity suggests that our universe is modelized by a four dimensional manifold equipped with a metric of signature (-,+,+,+), called Lorentzian metric, which satisfies Einstein equations. In 1969, Choquet-Bruhat and Geroch established the existence of a unique maximal development of a given initial data for the Einstein equations. These solutions fit within the general framework of globally hyperbolic spacetimes. There is a partial order relation on globally hyperbolic spacetimes. Following the work of Choquet-Bruhat and Geroch, the questions of the existence and the uniqueness of a maximal extension of a globally hyperbolic spacetime arise naturally. In this talk, I will discuss these questions in the context of globally hyperbolic conformally flat spacetimes. In 2013, C. Rossi positively answered both questions in this specific context. However, her proof has the unsatisfactory feature that it relies crucially on the axiom of choice through Zorn Lemma on the one hand. On the other hand, it does not provide any description of the maximal extension. I will present an alternative, constructive proof of this result. This approach is based on the concept of enveloping space, within which the maximal extension will be realized. After defining the enveloping space, I will illustrate this concept with some examples.

12:30 Lunch cocktail (Break room, IRMA)

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/16 …

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 this talk I 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 construct a partial formal proof of the Basel problem which follows the method of Euler's proof from his 'Introductio in Analysin Infinitorum'. Our proof utilises the concept of 'hidden lemmas' which was developed by McKinzie and Tuckey based on Lakatos and Laugwitz to represent general principles which Euler followed. We develop a theory of infinite 'hyperpolynomials' in Isabelle in order to formalise these hidden lemmas. Formal reconstruction of Euler's proof demystifies his reasoning and reveals mistakes in previous descriptions of his proof. We use our formalisation to demonstrate that Euler was systematic in his use of infinitely-small and large numbers, did not make unjustified leaps of intuition, and yet used distinct methodology to modern deductive proof.

About the speaker: Imogen Morris studied mathematics at the University of Edinburgh and continued there for her PhD research supervised by Jacques Fleuriot which this talk is based on. She now holds a postdoctoral position at the University of Edinburgh working on compound axiomatic memory models with Vijay Nagarajan, Tobias Grosser and Andrés Goens. Her research interests include nonstandard analysis, philosophy and history of mathematics, formalisation of mathematics in proof assistants and formal methods.