Marie Kerjean distinguée par la Fondation L'Oréal-Unesco

Une prépa à Paris et l’ENS Lyon en mathématiques. Le master MPRI à l'université Paris-Diderot. Une thèse en Informatique soutenue fin 2018 à l'Institut de Recherche en Informatique Fondamentale (IRIF). Puis un postdoctorat commencé il y a un an au sein de Gallinette, une équipe Inria/LS2N de Nantes spécialisée en particulier dans les assistants de preuve. 
Voilà pour le CV express de Marie Kerjean qui va devoir y rajouter une ligne : lauréate 2019 d'une Bourse L'Oréal-Unesco pour les Femmes et la Science.

Son domaine de spécialité se situe “à l'interface de la logique et des mathématiques.” 
Plus précisément, “cette partie de la logique qui parle de formules et de preuves. Je m'intéresse aux liens qu'elle présente avec l'analyse.” Alors que l'algèbre sert typiquement à l'étude des événements discrets, “l'analyse va permettre d'étudier les fonctions et leurs dérivées. Elle va aider, par exemple, à décrire des comportements physiques. Pour les lycéens en classe de première, c'est le fameux exercice sur le boulet de canon. Je vous donne un boulet, des conditions de départ et les contraintes qui s’exercent au cours du temps. Donnez-moi la fonction qui va décrire sa trajectoire dans l'espace. Voilà typiquement une question d'analyse. Je donne des contraintes. Décrivez-moi le mouvement continu. ”

Durant sa thèse, Marie Kerjean a étudié ces aspects logique et analyse en travaillant sur la sémantique. 
“Je m'intéressais à interpréter la logique dans des structures d’analyse fonctionnelle à travers une correspondance où l'on écrit les programmes comme des fonctions. On essaye de faire dire des choses à la logique à travers les mathématiques et vice versa. On se dit à la fois que les structures logiques sont intéressantes, qu'elles vont faire des nouvelles mathématiques, et que des concepts mathématiques peuvent être ré-implantés en logique. ”

Assistant de preuve Coq

Désormais, en postdoctorat, la jeune chercheuse participe à l’écriture de bibliothèques d'analyse pour Coq.

Créé il y a 25 ans par Inria, cet assistant de preuve est devenu un outil de premier plan dans son domaine. Il permet de prouver la correction des programmes informatiques et à ce titre intéresse l'industrie. Des groupes comme Airbus l'utilisent.

Mais il sert aussi en mathématiques pour prouver des théorèmes. 
“Il y a quelques années, par exemple, Georges Gonthier qui dirige le groupe Mathematical Components [du centre Microsoft-Inria] travaillant sur la formalisation de la théorie des groupes finis, a prouvé le théorème de l'ordre impair à l'aide de Coq. La démonstration en avait été faite dans les années soixante par les mathématiciens Feit et Thompson. Elle représentait alors plusieurs centaines de pages.”

“Coq se prête bien aux travaux en algèbre. Mais, a priori, il convient moins pour de l'analyse. Mon travail porte justement sur le développement de cet aspect analyse. Nous pensons que Coq est riche de sa proximité avec la certification de programmes. L'outil, basé sur la théorie des types dépendants, permet de réaliser des choses impossibles avec d'autres assistants à la preuve. 
Dans l'équipe Gallinette, sous la direction d'Assia Mahboubi, je participe donc à l'écriture de bibliothèques, typiquement sur l'analyse complexe. Nous les envisageons pour des formalisations mathématiques, mais elles pourraient être utilisées ensuite dans d'autres contextes par des industriels. Et c'est d'ailleurs ce qui m'intéresse le plus : développer des bibliothèques accessibles et utilisables par beaucoup de gens.”

Confrontation à l'ordinateur

Pour la chercheuse, écrire des mathématiques destinées à l'ordinateur constitue à la fois “un jeu et une confrontation. Nous sommes censés maîtriser des mathématiques que nous pratiquons depuis des années. Mais elles demeurent basées sur une pratique souvent moins formelle que celles auxquelles nous devons nous plier avec l'ordinateur. Par ailleurs, le domaine de la preuve repose sur la théorie des types, qui diffère de la théorie des ensembles avec laquelle on construit souvent les mathématiques. Quand on regarde un objet sous un point de vue, il possède une certaine forme. Sous un angle différent, il en a une autre. Or l'ordinateur ne va pas nous autoriser ce genre de flou sémantique. Il va falloir lui préciser toutes ces choses. En outre, les mathématiques devenant de plus en plus compliquées, il est facile de se laisser tellement absorber que l'on peut oublier un cas particulier. L'ordinateur permet de faire des mathématiques où il n'y a plus de doute sur le niveau de rigueur. C'est lui qui va vérifier que ce que vous prétendez être une preuve... en est bien une !”