Une formalisation de la déterminabilité de Borel en Lean

Informations fondamentales

• ID de l'article: 2502.03432
• Titre: Une formalisation de la déterminabilité de Borel en Lean
• Auteur: Sven Manthe
• Classification: math.LO (Logique mathématique)
• Date de publication: Février 2025 (prépublication arXiv)
• Lien de l'article: https://arxiv.org/abs/2502.03432

Résumé

Cet article formalise le théorème de déterminabilité de Borel dans le vérificateur de théorèmes Lean 4. Cette formalisation comprend la définition des jeux de Gale-Stewart et la preuve du théorème de Martin, qui établit que les jeux de Borel sont déterminés. La preuve suit étroitement la "preuve purement inductive de la déterminabilité de Borel" de Martin.

Contexte et motivation de la recherche

Contexte du problème

1. Importance de la théorie de la déterminabilité: La déterminabilité des jeux infinis à deux joueurs est un sujet central de la théorie descriptive des ensembles, introduite par Gale et Stewart en 1953
2. Fondements théoriques: Bien que la déterminabilité de grandes classes d'ensembles soit étroitement liée aux grands cardinaux, la déterminabilité de Borel peut être prouvée dans la théorie des ensembles ZFC
3. Défis de formalisation: La déterminabilité de Borel est connue pour nécessiter un fragment ZFC plus grand que la plupart des théorèmes courants, ce qui rend sa formalisation difficile

Motivation de la recherche

1. Première formalisation: Au-delà de la classe des ensembles fermés, la déterminabilité n'a jamais été formalisée dans un assistant de preuve
2. Vérification théorique: Vérifier que la théorie des types de Lean 4 est suffisante pour traiter les théorèmes nécessitant des fragments forts de la théorie des ensembles
3. Exploration technique: Explorer l'utilisation d'hypothèses propositionnelles plutôt que de "valeurs poubelles" dans la formalisation

Contributions principales

1. Première formalisation complète: Première formalisation dans un vérificateur de théorèmes d'un résultat de déterminabilité au-delà des ensembles fermés
2. Innovations techniques:
   • Introduction du concept de "déploiement universel" remplaçant l'induction transversale de Martin
   • Utilisation de méthodes de théorie des catégories pour traiter les constructions de limites inverses
   • Développement de stratégies d'automatisation pour traiter les applications k-fixes
3. Vérification des choix de conception: Preuve de la faisabilité d'utiliser des hypothèses propositionnelles plutôt que des "valeurs poubelles" pour implémenter les fonctions partielles
4. Envergure du code: Implémentation complète d'environ 5000 lignes de code, dont les définitions fondamentales représentent moins de la moitié

Détails méthodologiques

Définitions des concepts fondamentaux

Jeux de Gale-Stewart

• Structure du jeu: G = (T, P), où T est un arbre non vide élagué et P ⊆ T est l'ensemble des gains
• Règles du jeu: Deux joueurs (0 et 1) choisissent alternativement des éléments de sorte que la séquence finie résultante soit dans T
• Conditions de victoire: Le joueur 0 gagne si le jeu infini a ∈ P, sinon le joueur 1 gagne

Stratégies et déterminabilité

• Définition de stratégie: Une stratégie σ est une fonction qui associe à chaque position x du joueur i un successeur
• Stratégie gagnante: σ est une stratégie gagnante si tous les jeux cohérents avec σ sont gagnés par le joueur i
• Déterminabilité: Un jeu est déterminé si au moins un joueur possède une stratégie gagnante

Innovations techniques

1. Concept de déploiement universel

-- Définition du déploiement
def Unravelable (T : Tree A) (P : Set [T]) : Prop :=
  ∀ k : ℕ, ∃ (π : T' → T) (φ : Strategy T' → Strategy T), 
    IsKCovering k π φ ∧ IsClopen ([π]⁻¹(P))

-- Déploiement universel (innovation de cet article)
def UniversallyUnravelable (T : Tree A) (P : Set [T]) : Prop :=
  ∀ (π : T' → T) (φ : Strategy T' → Strategy T), 
    IsCovering π φ → Unravelable T' ([π]⁻¹(P))

2. Cadre de théorie des catégories

Définition d'une catégorie C dont les objets sont des paires (A,T) (T est un arbre sur A), et les morphismes sont des applications équi-longueur préservant la structure:

• Construction de limites: Preuve que C possède toutes les limites
• Propriétés fonctorielles: L'application de réalisation T ↦ T s'étend en un foncteur de C vers les espaces topologiques
• Couvertures k: Applications de couverture bijectives sur les k premiers niveaux

3. Structure des lemmes clés

Lemme 3.2 (Propriété σ-algèbre):

lemma universally_unravelable_sigma_algebra (T : Tree A) :
  IsSigmaAlgebra {P | UniversallyUnravelable T P}

Lemme 3.3 (Déploiement universel des jeux fermés):

lemma closed_games_universally_unravelable (T : Tree A) (P : Set [T]) 
  (h : IsClosed P) : UniversallyUnravelable T P

Stratégies de preuve

Construction de déploiement pour les jeux fermés

Dans le jeu déployé G':

1. Première étape: Le joueur 0 choisit non seulement le mouvement a₀, mais aussi sa quasi-stratégie σ
2. Deuxième étape: Le joueur 1 choisit soit une séquence finie x compatible avec σ (elle gagne dans tous les jeux étendant x), soit une quasi-stratégie garantissant l'échec de σ
3. Étapes suivantes: Les joueurs procèdent selon la stratégie choisie

Traitement des unions dénombrables

Utilisation de la construction de limite inverse:

... → T₃ → T₂ → T₁ → T₀

où chaque application de transition est une (k+i)-couverture, et les projections de la limite s'étendent en (k+i)-couvertures.

Configuration expérimentale

Environnement d'implémentation

• Vérificateur de théorèmes: Lean 4
• Bibliothèque mathématique: mathlib
• Envergure du code: Environ 5000 lignes
• Structure du projet: Définitions fondamentales (<50%) + formalisation de la preuve de Martin (>50%)

Défis techniques et solutions

1. Stratégies d'automatisation

Développement d'automatisations traitant deux classes d'hypothèses:

• Hypothèses de position: "x est une position du joueur i", réduction à l'arithmétique de Presburger
• Hypothèses k-fixes: Utilisation du mécanisme d'inférence de classes de types pour déduire automatiquement la valeur appropriée de k

class Fixing (k : outParam ℕ) (f : S → T) : Prop where 
  prop : IsIso ((res k).map f)

2. Traitement des types dépendants

Création d'une métaprogramme abstract pour abstraire avec impatience les termes de preuve en lemmes:

elab "abstract" tacs:ppDedent(tacticSeq) : tactic => do
  let target ← getMainTarget
  let goal ← getMainGoal
  let newGoal ← mkFreshExprMVar target
  setGoals [newGoal.mvarId!]
  Elab.Tactic.evalTactic tacs
  setGoals [goal]
  goal.assign (← mkAuxTheorem ((← getDeclName?).get! ++ 'abstract ++ (← mkFreshId)) target newGoal)

Résultats expérimentaux

Complétude de la formalisation

1. Vérification de complétude: Formalisation réussie de la preuve complète du théorème de Martin
2. Vérification des types: Toutes les définitions et tous les théorèmes passent la vérification des types de Lean 4
3. Compilabilité: L'ensemble du projet compile et se vérifie avec succès

Comparaison avec la preuve originale

1. Préservation de la structure: La structure de la preuve suit étroitement la preuve originale de Martin
2. Adaptation technique: Adaptation réussie de la preuve théorique des ensembles au cadre de la théorie des types
3. Améliorations innovantes: Évitement de l'induction transversale grâce au déploiement universel

Analyse de performance

1. Temps de compilation: Temps de compilation raisonnable (valeurs spécifiques non fournies dans l'article)
2. Utilisation mémoire: Évitement de la croissance exponentielle du temps d'exécution grâce à l'abstraction avec impatience
3. Efficacité de l'automatisation: Les stratégies développées réduisent considérablement le travail de preuve manuel

Travaux connexes

Formalisation de la théorie des jeux

1. Joosten (2021): Formalisation en Isabelle de la déterminabilité des jeux fermés
   • Utilisation de listes coinductives pour traiter simultanément les jeux finis et infinis
   • Cet article se concentre sur les jeux infinis, décrivant les jeux partiels uniquement avec des séquences finies
2. Mathlib: Contient des formalisations de jeux finis (SetTheory.Game), suivant l'approche de Conway
   • Traite uniquement les jeux finis
   • La déterminabilité est toujours satisfaite dans ce contexte

Théorie descriptive des ensembles

1. Résultats fondamentaux: mathlib contient déjà les résultats fondamentaux de la théorie descriptive des ensembles
2. Contenu manquant: Plusieurs corollaires de la déterminabilité de Borel restent à formaliser
3. Applications potentielles: Ce travail peut servir d'outil pour construire une bibliothèque plus complète de théorie descriptive des ensembles formalisée

Conclusion et discussion

Conclusions principales

1. Preuve de faisabilité: Démonstration que la formalisation de théorèmes nécessitant des fragments ZFC forts est possible en Lean 4
2. Validité de la méthode: La méthode purement inductive de Martin s'adapte avec succès au cadre de la théorie des types
3. Innovations techniques: Le concept de déploiement universel et les méthodes de théorie des catégories simplifient efficacement le processus de formalisation

Limitations

1. Limites de la force théorique: Les formes plus fortes de déterminabilité (comme la déterminabilité analytique) ne peuvent pas être prouvées sans axiomes supplémentaires
2. Complexité: La force théorique de la preuve se manifeste par la croissance rapide de la cardinalité des ensembles
3. Domaine spécifique: La méthode s'applique principalement aux problèmes de déterminabilité en théorie descriptive des ensembles

Directions futures

1. Extension de la déterminabilité: Formalisation de la déterminabilité de classes d'ensembles plus grandes sous des hypothèses de grands cardinaux
2. Résultats inverses: Formalisation des énoncés inverses construisant des modèles internes de grands cardinaux à partir de la déterminabilité
3. Amélioration de la bibliothèque: Utilisation de la déterminabilité de Borel pour construire une bibliothèque plus complète de théorie descriptive des ensembles formalisée

Évaluation approfondie

Avantages

1. Travail novateur: Première formalisation de la déterminabilité au-delà des ensembles fermés, d'une importance majeure
2. Profondeur technique:
   • Adaptation ingénieuse des preuves théoriques des ensembles à la théorie des types
   • Introduction innovante du concept de déploiement universel
   • Utilisation efficace de la théorie des catégories pour simplifier les constructions complexes
3. Qualité d'ingénierie:
   • 5000 lignes de code de haute qualité
   • Support d'automatisation complet
   • Optimisations de performance efficaces
4. Contributions méthodologiques: Perspectives précieuses pour traiter les fonctions partielles dans les types dépendants

Insuffisances

1. Limitations de documentation: Certains détails techniques pourraient être expliqués plus en détail
2. Données de performance: Absence de données de référence de performance concrètes
3. Extensibilité: L'extensibilité à des résultats de déterminabilité plus complexes n'a pas encore été vérifiée
4. Accessibilité: Accessibilité limitée pour les utilisateurs non spécialistes

Impact

1. Signification théorique:
   • Démonstration des capacités de la théorie des types à traiter les résultats forts de théorie des ensembles
   • Fourniture d'un modèle pour la formalisation de sujets avancés en mathématiques
2. Valeur pratique:
   • Établissement des fondations pour la formalisation ultérieure de la théorie descriptive des ensembles
   • Fourniture de techniques et de méthodes réutilisables
3. Reproductibilité:
   • Implémentation complète en open source
   • Documentation technique détaillée
   • Bonne intégration avec la bibliothèque standard

Scénarios d'application

1. Mathématiques formalisées: Applicable à la formalisation de théorèmes mathématiques nécessitant des fondements forts de théorie des ensembles
2. Recherche en théorie des jeux: Fourniture de fondations pour la formalisation de la théorie des jeux infinis
3. Recherche en logique: Fourniture d'outils pour étudier les relations entre déterminabilité et grands cardinaux
4. Applications pédagogiques: Peut servir de matériel pédagogique pour les cours avancés de logique mathématique

Références

Références clés

1. Martin, D. A. (1975): "Borel determinacy" - Preuve originale de la déterminabilité de Borel
2. Martin, D. A. (1985): "A purely inductive proof of Borel determinacy" - Référence principale suivie par cet article
3. Gale, D. & Stewart, F. M. (1953): "Infinite games with perfect information" - Définition originale des jeux de Gale-Stewart
4. Kechris, A. S. (1995): "Classical descriptive set theory" - Manuel classique de théorie descriptive des ensembles

Résumé: Cet article représente un travail d'importance majeure dans le domaine des mathématiques formalisées, formalisant avec succès un théorème profond nécessitant des fondements forts de théorie des ensembles dans le cadre de la théorie des types. L'article ne se contente pas d'être innovant sur le plan technique, mais fournit également des expériences et des méthodes précieuses pour les travaux connexes futurs. Malgré certaines limitations, ses contributions novatrices et son implémentation de haute qualité en font une étape importante dans le domaine des mathématiques formalisées.