Marie Kerjean awarded a L’Oréal - Unesco Foundation grant

Preparatory classes in Paris and at ENS Lyon in mathematics. A Master’s of Research in Computer Science (MPRI) at Paris-Diderot University. A PhD in IT completed in late 2018 at the Institut de Recherche en Informatique Fondamentale (IRIF - Research Institute on the Foundations of Computer Science), followed by a postdoctorate begun a year ago with Gallinette, an Inria/LS2N team in Nantes specialising in proof assistants. That is just a brief run-down of Marie Kerjean ’s CV, although she will soon be needing to add one more line: ‘awarded a L’Oréal-Unesco Grant for Women in Science in 2019’.

Her area of expertise lies at “the interface between logic and mathematics”. More specifically, “the area of logic which deals in formulas and proofs. I am interested in its links with analysis”. While algebra is typically used to study discrete events, “analysis makes it possible to study functions and their derivatives, to help describe physical behaviour, for example. One example of this is the well-known “cannonball exercise” given to sixth-year students in high school. If I give you a cannonball, some starting conditions and the constraints that will be applied over time, can you give me the function describing its trajectory through space? That's a typical analysis question. Here are some constraints, now describe the continuous movement.”

While studying for her PhD, Marie Kerjean carried out research into these logic and analysis aspects, working on semantics. “I was interested in interpreting logic in functional analysis structures through correspondence, writing programmes as functions. The aim is for logic to benefit from mathematics, and vice-versa. We feel that logical structures are of great interest, that they are going to lead to a new type of mathematics, and also that mathematical concepts can be re-introduced into logic.”

Coq proof assistant

Now a postdoc student, the young researcher is involved in writing analysis libraries for Coq. This proof assistant was created 25 years ago by Inria and has become a leader in its sector. It is capable of proving that computer programmes are correct and is therefore of interest to industry. It is used by groups such as Airbus, but it is also used in mathematics to prove theorems. “For example, a few years ago, Georges Gonthier, who headed the Mathematical Components group (at the Microsoft-Inria Centre) working on the formalisation of finite group theory, was able to prove the odd order theorem using Coq. This theorem had first been proven in the 1960s by mathematicians Feit and Thompson, at the time running to several hundred pages.”

“Coq lends itself well to use in algebra, but is less suited to analysis. My work involves developing its analysis capabilities. We feel that one of Coq’s strengths lies in its proximity to programme certification. The tool is based on dependent type theory and can be used to perform tasks that would be impossible using other proof assistants. In the Gallinette team headed by Assia Mahboubi , I take part in writing libraries, typically involving complex analysis. These libraries are initially conceived for mathematical formalisation, but they could also be used in other contexts by industrialists. This is what I find most interesting: developing libraries that are accessible and can be used by a lot of people.”

Going head-to-head with the computer

For this researcher, writing mathematics for computers is both “a game and a confrontation. We are expected to be adept at mathematics after years of work. The problem is that our mathematical practices are often less formal than those required for our work with computers. The field of proof also draws heavily on type theory, as opposed to set theory which is often used for mathematical construction. When we look at an object from one perspective, it has a certain shape. From a different angle, it takes on an entirely different one. The issue here is that the computer won't allow this type of semantic fuzziness. All of these things have to be explained to it. Plus, with mathematics becoming increasingly complex, it’s easy to become so absorbed in it that we forget an individual case. Computers can be used for mathematics when there is no longer any doubt as to the level of rigour. It is the computer that will check that what you consider to be proof really is!”