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