A formalization of Borel determinacy in Lean

Cet article présente une formalisation de la déterminance borélienne dans le prouveur de théorèmes Lean 4, incluant une définition des jeux de Gale-Stewart et une preuve du théorème de Martin suivant la méthode purement inductive de ce dernier.

L'essentiel

🎲 Le Grand Jeu de l'Infini : Comment un ordinateur a prouvé une vérité mathématique

Imaginez un jeu infini entre deux joueurs, disons Alice et Bob. Ils s'assoient devant un tableau et, tour à tour, ils choisissent des nombres. Ils continuent comme ça pour toujours, sans jamais s'arrêter. À la fin, ils ont produit une liste infinie de nombres.

La question est simple : L'un des deux joueurs a-t-il une stratégie infaillible pour gagner, peu importe ce que fait l'autre ?

C'est le cœur de ce que les mathématiciens appellent la déterminisme. Pour certains types de jeux, on sait que l'un des joueurs gagne toujours. Pour d'autres, c'est plus compliqué. L'article que nous allons explorer raconte l'histoire de la preuve que tous les jeux "Boreliens" (un type de jeu très courant et bien comporté) sont déterminés.

Mais il y a un twist : cette preuve n'a pas été faite par un humain avec un stylo et du papier, mais par un ordinateur utilisant un logiciel spécial appelé Lean.

1. Le Défi : Un labyrinthe mathématique

Pensez aux mathématiques comme à une immense bibliothèque. Certains livres (théorèmes) sont faciles à lire. D'autres, comme celui sur la "déterminisme des jeux Boreliens", sont des labyrinthes complexes qui nécessitent des outils très puissants.

L'auteur, Sven Manthe, a décidé de construire ce labyrinthe dans un langage que l'ordinateur comprend parfaitement. C'est comme si vous demandiez à un robot de vérifier chaque brique d'un château de cartes géant pour s'assurer qu'il ne s'effondrera jamais.

Pourquoi est-ce difficile ?
Parce que le jeu est infini. On ne peut pas jouer "jusqu'au bout" pour voir qui gagne. Il faut une logique mathématique très fine pour prédire le résultat sans jouer.

2. La Solution : Le "Démêlage" (Unraveling)

Pour résoudre ce casse-tête, l'auteur a utilisé une idée brillante du mathématicien Donald Martin. Imaginez que le jeu original est un nœud compliqué, un écheveau de laine emmêlé.

• L'idée : Au lieu de regarder le nœud de face, on essaie de le "démêler" en le projetant sur une autre surface plus simple, comme un tapis.
• L'analogie : Imaginez que vous avez une carte au trésor dessinée sur un papier froissé et déchiré (le jeu original). C'est dur à lire. Martin propose de transférer cette carte sur un grand drap blanc parfaitement lisse (un jeu "démêlé"). Sur ce drap, les règles sont si claires que l'on voit immédiatement qui gagne.
• Le résultat : Si on peut faire ce transfert (ce "démêlage") pour n'importe quel jeu Borelien, alors on sait que le jeu original est aussi gagnable.

L'auteur a codé cette idée de "démêlage" dans l'ordinateur. C'est comme si l'ordinateur apprenait à transformer un puzzle impossible en un puzzle facile, étape par étape.

3. Le Langage de l'Ordinateur : Lean

Lean est un "traducteur" très strict. Il ne tolère aucune ambiguïté.

• Le problème des "valeurs poubelles" : Dans les programmes informatiques classiques, si une fonction ne marche pas pour une certaine entrée, on lui donne souvent une valeur par défaut (comme mettre "0" ou "null" à la place). C'est comme si un cuisinier, s'il n'avait pas d'œufs, mettait un caillou dans la soupe et disait "c'est bon, c'est un œuf spécial".
• L'approche de l'auteur : Sven Manthe a refusé cette méthode. Pour lui, si une règle ne s'applique pas à une situation, il faut le dire explicitement. C'est comme dire : "Cette recette ne marche que si vous avez des œufs". Si vous n'en avez pas, la recette n'existe pas, on ne met pas de caillou.
• Pourquoi ? C'est plus proche de la façon dont les humains raisonnent en mathématiques. Cela rend le code plus logique, mais beaucoup plus difficile à faire accepter par l'ordinateur, car il doit vérifier des conditions à chaque étape.

4. Les Pièges de la Traduction

Le plus gros défi n'était pas la logique mathématique elle-même, mais la façon dont l'ordinateur la "pense".

• Le problème des types : En mathématiques, on dit souvent "Soit x un nombre pair". En informatique, si on change x, l'ordinateur doit vérifier que le nouveau x est toujours pair. C'est comme changer de pièce dans un jeu de construction : si vous changez une pièce bleue par une rouge, vous devez vérifier que le mur tient toujours.
• La performance : Parfois, l'ordinateur passait trop de temps à vérifier ces détails, comme un chien qui renifle chaque brindille avant de traverser une forêt. L'auteur a dû inventer de petits outils (des "scripts") pour dire à l'ordinateur : "Fais confiance, on sait que ça marche, passe à la suite !"

5. Pourquoi est-ce important ?

Avant ce travail, personne n'avait réussi à prouver ce théorème complexe avec un ordinateur. C'est une victoire majeure pour deux raisons :

1. La confiance : Cela prouve que les mathématiques modernes, même les plus abstraites, peuvent être vérifiées par des machines. Plus d'erreurs humaines cachées dans des calculs trop longs.
2. L'avenir : Cela ouvre la porte pour prouver d'autres théorèmes encore plus complexes sur les jeux infinis et les grands nombres infinis.

En résumé

Cet article raconte comment un chercheur a pris un théorème mathématique célèbre, mais très difficile (le jeu infini), et l'a traduit dans le langage d'un robot (Lean). Il a dû inventer de nouvelles façons de parler à l'ordinateur pour éviter les raccourcis dangereux, prouvant ainsi que même les jeux les plus complexes ont une issue certaine, et que l'ordinateur peut maintenant nous aider à le voir.

C'est un peu comme si on avait demandé à un robot de vérifier qu'un pont infini ne s'effondrerait jamais, et le robot a répondu : "Oui, j'ai vérifié chaque brique, et le pont est solide."

Résumé technique

Voici un résumé technique détaillé de l'article « A formalization of Borel determinacy in Lean » de Sven Manthe, rédigé en français.

1. Problématique et Contexte

La déterminabilité des jeux de Borel est un résultat fondamental de la théorie descriptive des ensembles, établi par Donald Martin en 1975. Elle stipule que tout jeu infini à deux joueurs (jeu de Gale-Stewart) dont l'ensemble des gains est un ensemble de Borel est déterminé (c'est-à-dire que l'un des deux joueurs possède une stratégie gagnante).

Bien que ce théorème soit démontrable dans la théorie des ensembles ZFC (Zermelo-Fraenkel avec l'axiome du choix), sa preuve est notoirement complexe et nécessite une grande puissance de déduction (beaucoup plus que la plupart des théorèmes standards). L'objectif de cet article est de présenter la première formalisation complète de la déterminabilité des jeux de Borel dans un assistant de preuve, spécifiquement dans Lean 4 et sa bibliothèque mathématique mathlib.

Le défi principal réside dans la nature de la preuve de Martin, qui repose sur une induction transfinie complexe et des constructions de limites inverses, ainsi que sur les défis techniques liés à la représentation des fonctions partielles et des types dépendants dans Lean.

2. Méthodologie

L'auteur suit de près la preuve de Martin présentée dans son article de 1985 (« A purely inductive proof of Borel determinacy »), tout en apportant des adaptations significatives pour s'adapter à la logique des types de Lean.

A. Définitions Fondamentales

• Jeux de Gale-Stewart : Formalisés comme des paires $(T, P)$ où $T$ est un arbre élagué (pruned tree) sur un ensemble $A$ et $P$ est l'ensemble des gains (une partie de l'espace des branches $[T]$).
• Stratégies : L'auteur choisit de représenter les stratégies comme des fonctions (stratégies fonctionnelles) associant à chaque position un ensemble de coups possibles, plutôt que comme des arbres de positions. Cette approche, bien que nécessitant plus de gestion des hypothèses de domaine, s'avère plus pratique pour la définition formelle.
• Propriété d'« Unravelability » (Démêlage) : Au lieu de prouver directement la déterminabilité, la preuve procède par induction sur la construction des ensembles de Borel en établissant une propriété plus forte : l'unravelabilité universelle. Un jeu est unravelable s'il existe un recouvrement (covering) vers un jeu dont l'ensemble des gains est ouvert-fermé (clopen).

B. Adaptations Techniques pour Lean

1. Induction sur la construction vs Induction transfinie :

   • La preuve originale de Martin utilise une induction transfinie sur la hiérarchie de Borel.
   • Manthe remplace cela par une induction directe sur la construction des ensembles de Borel. Pour cela, il introduit le concept de « unravelabilité universelle » (universal unravelability), qui est plus forte que l'unravelabilité simple. Cela permet de montrer que l'ensemble des jeux unravelables universellement forme une $\sigma$-algèbre, évitant ainsi l'utilisation explicite d'ordinaux dans la récursion.

2. Limites Inverses et Théorie des Catégories :

   • La preuve pour les unions dénombrables nécessite la construction d'une limite inverse de jeux.
   • L'auteur formalise la catégorie $\mathcal{C}$ des arbres et utilise la bibliothèque de théorie des catégories de mathlib. Il démontre que les limites existent dans cette catégorie et que les projections sont des recouvrements $k$-fixants (k-fixing), une étape cruciale pour stabiliser les niveaux de l'arbre.

3. Gestion des Fonctions Partielles :

   • Une décision de conception majeure est le rejet de la convention de mathlib qui utilise des « valeurs poubelles » (junk values, ex: 0 pour un élément hors domaine) pour les fonctions partielles.
   • L'auteur adopte l'approche mathématique standard : une fonction partielle est représentée par une fonction dont le domaine est restreint par une hypothèse propositionnelle (ex: ∀x, P(x) → Y).
   • Cela permet de respecter la sémantique mathématique (une stratégie n'est pas définie pour les coups de l'adversaire), mais pose des défis techniques pour les tactiques de réécriture dans Lean.

3. Contributions Clés

• Première formalisation au-delà des jeux fermés : C'est la première fois qu'un résultat de déterminabilité pour une classe de jeux plus large que les jeux fermés (ouverts) est formalisé dans un assistant de preuve.
• Implémentation de la preuve de Martin : Le code (environ 5 000 lignes) formalise intégralement la preuve de Martin, y compris les constructions complexes de limites inverses et de recouvrements.
• Développement de tactiques personnalisées :
  • Création de tactiques pour gérer automatiquement les hypothèses de parité (pour déterminer quel joueur joue) et les propriétés « k-fixing » des morphismes, utilisant l'inférence de classes de types (typeclass inference) de Lean.
  • Développement d'un métaprogramme (abstract puis as_aux_lemma) pour résoudre les problèmes de performance liés à la taille exponentielle des termes de preuve lors de l'usage de types dépendants profonds.
• Analyse comparative des approches de fonctions partielles : L'article fournit une analyse détaillée des avantages et inconvénients de l'approche par hypothèses propositionnelles (préférée ici) par rapport à l'approche par valeurs poubelles (préférée par mathlib).

4. Résultats

• Théorème 2.1 (Déterminabilité de Borel) : Le théorème est prouvé dans Lean 4.
• Lemmes Techniques :
  • Lemme 2.2 : Pour un arbre fixe $T$, l'ensemble des ensembles de gains $P$ tels que $(T, P)$ est universellement unravelable forme une $\sigma$-algèbre.
  • Lemme 2.3 : Les jeux fermés sont universellement unravelables.
• Performance : L'auteur a dû surmonter des goulots d'étranglement de performance causés par la récursion sur les termes de preuve dans les types dépendants. L'utilisation de son outil d'abstraction a permis de réduire la complexité temporelle de manière significative.

5. Signification et Impact

• Puissance de la théorie des types : L'article démontre que la théorie des types de Lean (équiconsistante avec ZFC + existence de cardinaux inaccessibles) est suffisamment puissante pour formaliser des théorèmes nécessitant une grande force de déduction, sans avoir besoin d'axiomes supplémentaires pour la déterminabilité de Borel.
• Avancement de la théorie descriptive des ensembles : Ce travail pose les bases pour formaliser des résultats plus avancés, comme la déterminabilité analytique (sous hypothèses de grands cardinaux) ou la construction de modèles internes.
• Débat sur la formalisation : L'article remet en question la convention de mathlib concernant les fonctions partielles. L'auteur soutient que l'approche par restriction de domaine (types dépendants) est plus naturelle mathématiquement et que les difficultés techniques actuelles de Lean (tactiques de réécriture, performance) sont des obstacles surmontables qui devraient être levés par l'évolution de l'outil, plutôt que par une adaptation des mathématiques à l'outil.

En résumé, ce travail est une avancée majeure en théorie des preuves formelles, combinant une profondeur mathématique significative (théorie des jeux, théorie descriptive) avec une ingénierie logicielle rigoureuse pour surmonter les limitations actuelles des assistants de preuve.