Conférences (Rapports L3) 1er Septembre

Assistants de preuves

Assia Mahboubi

Qu’est-ce qu’un théorème ? Ne pas négliger le caractère “social” du processus

Qu’est-ce qu’un programme informatique ? Comment le vérifier ? :

  • Spécification ex: métro 14 à Paris ⟹ sans conducteur ⟹ vérification formelle

ex: conjecture de Goldbach faible :

tout entier $\geq 7$ est la somme de trois nbs premiers

ex: V. Voevodsky : affecté par le fait qu’un de ses artciles faux ait été publié du fait qu’il était médaillé Fields (2002)

  • Leibniz : idée d’utiliser une “langue rigoureuse”

MAIS : Bourbaki contre ça (cf. “L’architecture des mathématiques”) : la vue d’ensemble de l’abstraction mathématique est perdue dans la vérification de preuve

MAIS : ce texte de B est incomplet : la tâche est réalisable sans que ce soit ennuyeux/stérilisant

Machine checking

Idée : écrire un programme unique qui permette de vérifier n’importe quelle preuve ⟹ appelé un assistant de preuve (AP)

Squelette d’un AP:

  • Logique formelle : ∃ différentes
  • Partie “assistant”

ex: Théorème des 4 couleurs, théorème de Kepler (oranges)

ex: Th de l’ordre impair :

Tout groupe d’ordre impair est résoluble

Tout groupe fini simple (sans ss-groupe distingué) de cardinal impair est cyclique

Théorie des types

Langage formel qui fonde les AP. Zermelo, et Russel (dans deux articles distincts)

ex: f : ℝ ⟶ ℝ, x \mapsto x+1

ex: ℙ_y(x) ≔ x \text{ is an odd multiple of } y

Attention au paradoxe du menteur !

Q’est-ce qu’un énoncé mathématique ? Un terme =

  • une variable
  • une fonction $𝜆 x \mapsto t$ OU $𝜆x.t$
  • une fonction appliquée à un terme
  • une constante

ex :

$𝜆x.t(u)$ donne $t$

𝛥 ≝ 𝜆x.x $𝛥$ appliqué à lui-même donne ?

Types = étiquettes 𝜆x.x : 𝛼 → 𝛼

Pb : $𝛥$ pas typable

Ex:

𝛤 \vdash t : 𝛼 → 𝛽 \, , \, 𝛤 \vdash u : 𝛼 donne (barre verticale) 𝛤 \vdash t(u) : 𝛽

Règles sont formalisées : ex: Modus Ponens

Règle de l’implication : 𝛤 𝛼 \vdash 𝛽 donne 𝛤 \vdash 𝛼 ⇒ 𝛽

⟹ Correspondance de Curry-Howard

Types dépendants

Familles de types qui dépendent de termes

Structure de donnée pour les énoncés mathématiques

ex: $A ⟹ B$ donne $A ⟶ B$

Comment passer de la logique formelle [Bas niveau] à (via l’assistant de preuve) une démo math [Haut niveau]

Il ne faut pas réinventer la roue ⟹ intérêt des bibli

Leave a comment