Qu'est-ce qu'un assistant de preuve ?

24 septembre 2023 — Logique, Lean

Je souhaiterais parler ici du concept et de la mise en œuvre des assistants de preuve (proof assistant).

Ce concept ne date pas d’hier (Coq, l’un des plus connus, a vu le jour en 1989), et reste un sujet de recherche actif aujourd’hui.

Différentes raisons peuvent amener à s’intéresser à ce sujet, par exemple :

• Sur le plan mathématique, c’est une façon pratique de commencer à s’intéresser au domaine de la logique.
• Pour des informaticiens, les assistants de preuve modernes mettent en œuvre des concepts de programmation qui sont également utilisés dans le cadre de la vérification de programmes.
• Plus récemment, les LLM laissent entrapercevoir des capacités de raisonnement. Les faire s’exprimer dans un langage formel permettrait une validation, impossible avec le langage courant — on pourra lire cette publication de OpenAI.

Je dois préciser que je ne suis pas expert du domaine : je ne m’y suis intéressé que récemment, et je souhaite synthétiser ici ma compréhension en commençant par des exemples simples.

Qu’est-ce qu’un assistant de preuve ?

Un assistant de preuve est un logiciel qui (a minima) permet de saisir un énoncé mathématique (une proposition), une preuve de cette proposition, et de vérifier automatiquement la validité de cette preuve.

Le langage dans lequel ces propositions et preuves sont saisies dépend du logiciel utilisé. Idéalement, on doit pouvoir faire correspondre aux formules mathématiques (e.g. $\forall a, -(-a) = a$) une formule de même signification et de syntaxe proche dans le langage de l’assistant.

Je ne souhaite pas ici définir trop précisément ce qu’on entend par logique mathématique (on pourra lire un article précédent à ce sujet), considérons juste que l’on a les concepts suivants :

• Des propositions, qui sont des énoncés mathématiques.
• Des axiomes, qui sont des propositions que l’on décrète vraies.
• Des règles d’inférence, qui permettent de démontrer des propositions (qui sont alors des théorèmes) à partir d’autres propositions (notamment les axiomes), et ainsi de construire des preuves.

Un intérêt d’une telle formulation des mathématiques est qu’on évite les ambiguïtés de la langue courante et qu’on peut mécaniser le processus de vérification de preuve. Nous allons voir sur un exemple simple à quoi tout ceci peut ressembler.

Un « modèle-jouet »

La structure mathématique d’anneau unitaire correspond à une axiomatisation de certaines propriétés des entiers (relatifs) vis-à-vis de l’addition, la soustraction et la multiplication.

Un ensemble (dont 0 et 1 désignent deux éléments particuliers et sur lequel on suppose définies des fonction $+$, $-$ et $\times$) est un anneau unitaire s’il vérifie les 9 axiomes suivants, $a, b, c$ désignant des éléments quelconques de cet ensemble :

La proposition $-(-a) = a$, qui nous semble évidente lorsqu’on a l’habitude de calculer avec des entiers, ne fait pas partie de ces axiomes. Elle en est cependant une conséquence comme le montre la preuve suivante :

Dans la preuve ci-dessus, on a utilisé successivement les axiomes 2, 4, 3, 1, 3 et 2. Vous pouvez la valider sur cette page, à l’aide d’un simple programme en JavaScript.

Ce programme, bien que limité (il ne fonctionne que pour les axiomes d’anneau unitaire), constitue un premier exemple d’assistant de preuve.

Son auteur l’a écrit pour vérifier les réponses à une question sur codegolf.stackexchange.com consistant à chercher la preuve la plus courte possible de la proposition ${(-a) \times (-a) = a \times a}$ (oui, c’est un peu geek…).

Formalisation avec Lean

En pratique, beaucoup d’assistants de preuve — notamment Lean et Coq — définissent des langages de programmation généraux, qui peuvent être utilisés en dehors du cadre mathématique.

La conception de ces langages est telle que les notions de proposition mathématique et de preuve s’y intègrent naturellement.

Ci-dessous, j’ai essayé de formaliser notre théorème avec Lean, et d’y implémenter la preuve vue plus haut (en fait, elle est un peu plus longue car Lean n’a pas défini le même jeu d’axiomes, mais peu importe) :

import Mathlib.Algebra.Ring.Basic
variable [Ring R] -- R is implicit
theorem first_theorem(a : R): -(-a) = a :=
calc
  -(-a) = -(-a) + 0             := by rw [add_zero]
    _   = 0 + -(-a)             := by rw [add_comm]
    _   = (a - a) + (-(-a))     := by rw [sub_self]
    _   = (a + (-a)) + (-(-a))  := by rw [sub_eq_add_neg]
    _   = a + ((-a) + -(-a))    := by rw [add_assoc]
    _   = a + (-a - (-a))       := by rw [sub_eq_add_neg]
    _   = a + 0                 := by rw [sub_self]
    _   = a                     := by rw [add_zero]

Vous pouvez tester ce programme sur cet éditeur en ligne : s’il ne s’affiche rien, c’est que le programme est accepté, sinon, vous verrez du rouge apparaître (essayez par exemple de changer un + en -). En cliquant sur certains éléments (par ex. add_zero), vous pourrez en voir la définition.

Quelques remarques sur ce code :

• On importe Mathlib.Algebra.Ring.Basic défini dans la bibliothèque mathlib.
• Notre théorème est défini comme une fonction qui prend en argument un élément a d’un anneau quelconque R et renvoie un objet de type -(-a) = a (qu’est-ce donc ?)
• L’implémentation de cette fonction constitue la preuve du théorème.

Ces deux dernières remarques méritent d’être détaillées, et nous y reviendrons plus loin. Pour l’instant, nous allons tenter de simplifier notre démonstration en utilisant une tactique.

Une tactique consiste à laisser l’assistant construire tout ou partie de la preuve par lui-même, en lui passant éventuellement quelques indications.

Un exemple de tactique est simp, qui va essayer de prouver la proposition en essayant de la simplifier grâce aux règles à sa disposition (axiomes et lemmes), en procédant plus ou moins par force brute (avec quelques heuristiques).

Bien sûr, ça ne fonctionne pas tout le temps, mais pour un théorème très simple comme le nôtre, cette tactique aboutit :

theorem first_theorem(a : R): -(-a) = a := by simp

Elle permet aussi de prouver un autre théorème mentionné plus haut (résultat) :

theorem second_theorem(a : R): (-a)*(-a) = a*a := by simp
#print second_theorem

Si vous cliquez sur la ligne qui affiche le théorème généré, vous verrez que celui-ci comporte bien une preuve (présentée d’une façon assez illisible…), basée sur des axiomes et lemmes de la théorie des anneaux.

Ci-dessous, j’ai essayé de prouver le théorème de théorie des groupes qui affirme que l’inverse $a^{-1}$ d’un élément $a$ est unique :

import Mathlib.Algebra.Group.Basic
variable [Group G]
theorem unique_inverse(a b c : G)(h1 : a * b = 1)(h2 : a * c = 1) : b = c := by simp

Je vous invite à observer la façon dont ce théorème est formulé, c’est-à-dire le type de unique_inverse — j’en dirai un mot plus loin.

Comme vous pouvez le constater, la tactique simp échoue à le démontrer (il faut cliquer sur simp souligné en rouge pour voir le message d’erreur).

En ajoutant quelques étapes manuellement, on obtient une preuve acceptée (je vous laisse cliquer sur les différentes lignes pour voir les manipulations correspondantes) :

import Mathlib.Algebra.Group.Basic
variable [Group G]
theorem unique_inverse(a b c : G)(h1 : a * b = 1)(h2 : a * c = 1) : b = c := by
  rw [<-h1] at h2
  simp at h2
  rw [h2.symm]

Vers une formalisation des mathématiques ?

Comme on peut déjà s’en rendre compte sur les cas qui précèdent, pourtant très simples, la formalisation des preuves peut vite devenir fastidieuse : ce qu’on considère comme une “évidence” dans une démonstration informelle demande parfois plusieurs dizaines d’étapes de formalisation.

La démonstration de l’irrationalité de $\sqrt{2}$ demande par exemple (au moins) une centaine de lignes — cela dépend évidemment des lemmes que l’on s’autorise — alors qu’elle s’exprime de façon plutôt concise dans le langage courant.

Elle fait partie de cette liste qui recense 100 théorèmes classiques et leurs preuves en Lean.

Le projet Fermat’s Last Theorem for regular primes (cas particulier du grand théorème de Fermat), lancé par le mathématicien Riccardo Brasca, est un exemple intéressant de théorème non trivial en cours de formalisation avec Lean.

Quelques concepts généraux

Ce qui suit est une présentation plus générale de concepts mis en œuvre dans certains assistants (notamment Lean et Coq), qui apportera peut-être un éclairage sur quelques subtilités de Lean constatées précédemment.

Les types dépendants

Nous avons défini notre premier théorème sous la forme d’une fonction de signature :

theorem first_theorem(a : R): -(-a) = a

Il s’agit du type des fonctions qui prennent en entrée un argument a de type R (où R représente un anneau quelconque) et retournent un objet de type -(-a) = a.

Ce type, qui dépend d’une valeur, est ce qu’on appelle un type dépendant.

C’est une construction qui peut être intéressante pour garantir certaines propriétés d’un programme, au-delà du cadre des preuves mathématiques.

Propositions as Types

Le type (dépendant) -(-a) = a représente une proposition (portant sur a), dont la signification est assez claire du fait de la syntaxe utilisée.

Cette idée de représenter les propositions comme des types de données trouve son inspiration dans une correspondance formelle — l’isomorphisme de Curry-Howard — entre logique et théorie des types.

J’insiste sur le terme inspiration car, pour que cette correspondance soit réellement un isomorphisme, il faut considérer certaines logiques et certaines théories des types — ni Lean ni Coq ne s’inscrivent strictement dans ce cadre.

Je cite ce passage d’une entrée du blog de Lawrence Paulson :

Proof assistants do not actually use propositions as types for the same reason that functional programming languages do not actually use the λ-calculus: because something that is beautiful in theory need not have any practical value whatever. It is still possible to take inspiration from the theory.

Ceci étant précisé, voici une liste informelle et non exhaustive de concepts logiques et leurs correspondants (via Curry-Howard) côté programme :

La curryfication

Dans le cadre de la correspondance de Curry-Howard, la proposition logique ${((P \land Q) \implies R) \iff (P \implies (Q \implies R))}$ correspond aux transformations entre types de fonctions que sont la curryfication et son inverse (la “décurryfication”).

Notre théorème unique_inverse est formulé en utilisant ce concept.

Digression sur le cas du Σ type

Je ne détaille pas tous les termes mentionnés ci-dessus, mais je vais tout de même parler du Σ type (ou type des paires dépendantes), qui n’est pas une construction très commune (contrairement par exemple au type union, que l’on retrouve même dans Python).

Ceci nous permettra aussi de donner une idée des subtilités liées à la correspondance de Curry-Howard.

Un Σ type, construit à partir d’un type A et d’un type dépendant B(a : A), est un type dont les valeurs correspondantes sont des paires (a, b), avec les typages a : A et b : B(a).

La correspondance de Curry-Howard associe à la proposition $\exists a \in A, P(a)$ le Σ type construit à partir des types A et P(a: A). Un programme prouvant $\exists a \in A, P(a)$ renvoie donc une paire (a, b) telle que a : A et b : P(a).

On l’interprète en disant que a est un témoin (de l’existence) et b est une preuve que ce témoin satisfait la propriété (représentée par P(a)).

Le problème avec cette interprétation du quantificateur existentiel, c’est qu’elle n’est pas celle de la logique classique, qui n’exige pas que l’on puisse construire un témoin.

L’exemple ci-dessous devrait vous en convaincre.

Une preuve non constructive

Théorème : Il existe des nombres irrationnels $x, y$ tels que $x^y$ soit rationnel.

Preuve : On pose $u = \sqrt{2}^{\sqrt{2}}$. Si $u$ est rationnel, on considère ${(x,y) = (\sqrt{2}, \sqrt{2})}$. Sinon, on remarque que ${u^{\sqrt{2}} = \sqrt{2}^2 = 2}$ et on considère ${(x,y) = (u, \sqrt{2})}$.

Cette preuve est valide au sens de la logique classique et pourtant, elle ne retourne pas de témoin : elle montre juste que l’un des couples ${(\sqrt{2}, \sqrt{2})}$, ${(\sqrt{2}^{\sqrt{2}}, \sqrt{2})}$ convient.

J’ai aussi (surtout ?) utilisé, sans le nommer, le principe du tiers-exclu, qui est un sujet épineux de la correspondance de Curry-Howard.

Ce que nous suggère cet exemple est que l’isomorphisme de Curry-Howard (tel que présenté ici) fait référence à une logique qui n’est pas la logique classique, puisque la preuve ci-dessus n’y est pas valide : c’est la logique intuitionniste.

Je ne souhaite pas développer plus les considérations logiques ici, je vous invite à lire cette entrée du blog de David Madore pour en apprendre davantage.

En pratique, Lean permet (aussi) de raisonner avec la logique classique, et les propositions existentielles n’y sont pas représentées par des paires dépendantes.

Voici par exemple une implémentation (exécuter) de la démonstration (non constructive) décrite plus haut et qui utilise la tactique by_cases :

import Mathlib.Data.Real.Irrational
import Mathlib.Analysis.SpecialFunctions.Pow.Real
open Real
lemma simple_lemma: ((sqrt 2)^(sqrt 2))^(sqrt 2) = 2 := by
  rw [<-rpow_mul]
  norm_num
  exact Real.sqrt_nonneg 2
theorem existence_theorem:
  ∃ x y : ℝ, (Irrational x) ∧ (Irrational y) ∧ ¬(Irrational (x^y)) := by
  by_cases h : Irrational ((sqrt 2)^(sqrt 2))
  -- h : Irrational (sqrt 2 ^ sqrt 2)
  {
    existsi (sqrt 2)^(sqrt 2), sqrt 2
    simp [h, simple_lemma, irrational_sqrt_two]
    exact Rat.not_irrational 2
  }
  -- h : ¬Irrational (sqrt 2 ^ sqrt 2)
  {
    existsi sqrt 2, sqrt 2
    simp [h, irrational_sqrt_two]
  }

Modification [11/11/2023] : Tous les exemples ont été convertis de Lean 3 à Lean 4.

Maths et applications, avec les mains et avec du code 💻
Suivre sur Twitter

• ← Autour des harmoniques sphériques
• Théorie des corps, continu et discret →