Le lambda-calcul et la formalisation des maths
avec Marco

Marco est arrivé à Nice en 2001 comme post-doc du CNR italien,
pour faire de la géométrie algébrique sous ma responsabilité.
Un peu par hasard, il a suivi mon cours de DEA sur le lambda-calcul,
et nous avons rapidement constaté tous les deux que
ce sujet lui convenait encore mieux que la géométrie algébrique.
Depuis, genre vers 2003, il a obtenu un post-doc CNRS d'un an
pour faire de la formalisation des maths sous ma responsabilité.
La consigne du CNRS etait qu'il fallait absolument le caser après.
C'était un peu stressant mais finalement, l'année suivante,
il a gagné un poste permanent de chercheur à Florence.

Mon projet avec Marco est un de mes trois projets prioritaires.
Il s'agit de domestiquer les ordinateurs pour qu'on puisse faire nos maths avec. Voici où on en est.

Notre premier travail est plus ou moins terminé. On y trouve une
approche originale à la fois de la syntaxe abstraite d'ordre supérieur et du lambda-calcul (pur)
que nous caractérisons comme la monade "exponentielle" initiale.

On savait depuis longtemps qu'un lambda-calcul typé est plus ou moins une catégorie cartésienne close, mais on n'avait rien de tel pour les lambda-calculs non typés.

La question de maitriser la syntaxe avec lieurs (syntaxe d'ordre supérieur)
est une question brûlante en informatique, voir par exemple le Poplmark challenge.
D'ailleurs, pour vérifier que notre approche est performante, nous avons nous-mêmes programmé une
solution de la partie A1 de ce challenge, que nous sommes en train de peaufiner avant soumission.

Il y a bientôt deux ans que nous avons compris notre caractérisation du lambda-calcul et
il nous a fallu tout ce temps pour en terminer la preuve sur ordinateur.
Il s'agit sans doute de l'énoncé le plus abstrait prouvé sur ordinateur.
Nous manipulons des monades et des morphismes entre modules sur des monades alors que
les tours de force qu'on connaît (théorème fondamental de l'algèbre, théorème des quatre couleurs,
théorème de Jordan sur les courbes planes)
ne manipulent pas des structures aussi abstraites.

Pour se faire une petite idée de ce travail, on peut
Ce travail n'est qu'un début. Voici les directions dans lesquelles on s'est déjà engagés.