We invite you to join us to our monthly Artificial Intelligence Meeting (AIM) at Observatoire astronomique de Strasbourg.

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)