Deux choses à distinguer

Démonstration automatique

L’humain fournit l’énoncé, le programme démontre (ou réfute).

Calculer des valeurs de vérité : (V ∨ F) ∧ (F ∨ V ∨ F) → V
Appliquer des procédures de décision
Rechercher des démonstrations automatiquement

Démonstration assistée

L’humain construit la démonstration avec l’aide du programme

Écrire une démonstration dans un langage formel, la faire vérifier
Manipuler des démonstrations comme des objets
Programmer pour élaborer des démonstrations

Faut-il parler d’intelligence artificielle ?

La recherche de preuve s’est développée dans le mouvement de l’IA symbolique des années 1960 et 1970.
Les systèmes d’IA générative sont efficaces pour produire des choses vraisemblables, mais sont difficilement explicables.
L’association des deux peut produire de nouvelles démonstrations valides.

Le théorème des quatre couleurs

Théorème

Toute carte planaire peut être coloriée en au plus 4 couleurs de sorte que deux régions limitrophes soient toujours de couleurs différentes.

Conjecturé dans la deuxième moitié du XIXème siècle (Möbius, Guthrie 1852)
Plusieurs démonstrations partielles (Kempe 1879, Tait 1880, …)
Première démonstration complète publiée en 1976 par Appel et Haken.
- Réduction à 1478 cas critiques
- Énumération et vérification des cas par un programme en langage machine sur un IBM 370/168 (1200 heures de calcul)
- Un certain émoi dans la communauté mathématique

Démonstration vérifiée formellement en 2005 par Gonthier et Werner.
- Formalisée avec Coq, avec toute la théorie nécessaire
- La validité des algorithmes d’énumération et vérification est formalisée
- Reconnu comme un tour de force technique
Aucune démonstration sans ordinateur n’est actuellement connue.

Les ∞-groupoïdes

Une autre histoire de démonstration assistée par ordinateur :

1990 : publication par Voevodsky et Kapranov de “∞-groupoids as a model for a homotopy category”
1998 : publication par Simpson de “Homotopy types of strict 3-groupoids”
— contient un contre-exemple au théorème principal de Voevodsky et Kapranov
Aucun ne parvient à pointer une erreur précise dans le papier de l’autre
Le doute s’installe sur le théorème de 1990
2013 : Voevodsky reconnaît que la démonstration de 1990 contient une erreur
S’ensuit un mouvement de formalisation en théorie homotopique des types.
Les résultats sont publiés avec leur démonstration formalisée en Coq.

The unreasonable effectiveness of mathematical experiments : what makes mathematics work
Asvin Gothandaraman, 2025

Quelle validation des résultats mathématiques ?

La réputation des mathématiciens peut aider à faire accepter des résultats très techniques et difficiles à vérifier.
Plus les objets sont d’un haut niveau d’abstraction, plus l’intuition peut être trompeuse.
La possibilité de développer des arguments jusqu’aux axiomes et principes logiques reste un critère de validation.

Ce qui fait preuve

Les caractéristiques d’une démonstration

Les traits qui font qu’un argument est une démonstration mathématique :

convaincant pour l’audience visée
expertisable par la communauté – évaluation par les pairs
formalisable en pratique ou en principe

The four-color problem and its philosophical significance
Tymoczko, 1979

Ces idées se sont développées après les débuts de la démonstration assistée par ordinateur.

Quel est le statut du programme informatique dans la démonstration du théorème des quatre couleurs par Appel et Haken ?
Quel est le statut de l’écosystème logiciel dans une démonstration formalisée dans un assistant aujourd’hui ?
Que gagne-t-on à déplacer le besoin de confiance vers un artefact technique ?

On est confronté à un nouvel aspect expérimental dans la pratique mathématique.

Petite histoire de la démonstration formalisée

Préhistoire

Avant l’ordinateur

‒300	Aristote	syllogistique
‒300	Euclide	démarche axiomatique
1666	Leibniz	Calculus ratiocinator
1879	Frege	Begriffsschrift
1910	Russell, Whitehead	Principia Mathematica
1920	Hilbert	problème de la décision
1931	Gödel	théorèmes d’incomplétude
1934	Gentzen	systèmes de déduction
1936	Church, Turing	résultats d’indécidabilité
~1960	Curry, Howard	correspondance preuve-programme

Les motivations derrière ces travaux :

caractériser les raisonnements valides
permettre des démonstrations libérées de l’intuition
certifier la cohérence de l’édifice mathématique
calculer la vérité des assertions formalisées

Euclide

Extrait d’une traduction française des Éléments d’Euclide

Frege

Exemple de démonstration dans le Begriffsschrift, 1879

Russell & Whitehead

Extrait des Principia Mathematica, 1910

Les assistants de preuve

Quelques outils marquants

1967	Automath	De Bruijn	première réalisation opérationnelle
1973	LCF	Milner	programmation de tactiques
1973	Mizar	Trybulec	style proche de l’écriture mathématique
1986	Isabelle	Paulson	adaptable à différentes logiques
1989	Coq	Coquand, Huet	extraction de programmes
2013	Lean	De Moura	ingénierie, passage à l’échelle

Il y en a beaucoup d’autres.

Ce qui change d’un système à l’autre :

le style privilégié : déclaratif ou impératif
la logique sous-jacente : classique, constructive, etc.
les bibliothèques mathématiques : choix de formalisation, corpus disponible
la communauté qui le porte : informaticiens ou mathématiciens

Ce sont tous des outils pour experts, il y a aussi des outils développés pour l’enseignement.

Pourquoi faire des démonstrations ?

La démonstration comme activité

Les rôles de la démonstration

valider des assertions (vérification, explication)
communiquer (systématisation, transmission à une communauté)
participer au processus de recherche (exploration de théories, élaboration de conjecture)

Proof, explanation and exploration : an overview
Hanna, 2000

Types de raisonnement impliqués dans l’activité de démonstration :

déductif
abductif
inductif
conceptualisation
recherche de contre-exemples
…

Types de raisonnement impliqués dans une démonstration formalisée :

déductif

La démonstration en classe

Pourquoi démontrer en classe

statut des énoncés mathématiques
formes de validation pour des notions abstraites
compréhension des notions mathématiques

Comment enseigne-t-on la démonstration ?

par imitation de pratiques exemplaires
par des situations qui nécessitent l’étude logique systématique
par la transition progressive de l’argumentation et de l’explication à la démonstration

Processus de preuve et situations de validation
Balacheff, 1987

La transition de la fin du lycée au début du supérieur est une étape critique.

Des assistants de preuve pour enseigner

Différentes tentatives, dans le but de s’attaquer aux difficultés des étudiants :

par des experts en logique et langages de programmation, depuis 1975
pour enseigner la logique, les mathématiques ou l’informatique
avec de outils et des interfaces spécifiques, par dessus des outils généraux ou comme des systèmes spécifiquement conçus

We already have some sense that proof assistants greatly diminish the need for verification and justification, but we know almost nothing of their potential contribution to other roles of proof, such as explanation, communication, discovery, and systematization, or how they now may become more relevant as pedagogical motivation for the learning of proof in the classroom.

Proof Technology in Mathematics Research and Training
Hanna, Reid & de Villiers, 2019

Quels sont les objectifs actuels de l’utilisation d’assistants de preuve dans l’enseignement ?

enseigner les assistants de preuve – cours de méthodes formelles dans les cursus d’informatique ou de mathématiques avancées
enseigner la démonstration mathématique – différentes expériences dans les premières années d’université

Utilisation des assistants de preuves pour l’enseignement en L1
Kerjean, Le Roux, Massot, Mayero, Mesnil, Modeste, Narboux & Rousselin, 2022.

L’interaction dans l’activité de démonstration

Une tâche de démonstration dans une situation d’enseignement implique idéalement :

l’exploration, la démarche essai-erreur, la formulation de conjectures ;
le débat contradictoire pour
- éprouver ses arguments et les améliorer,
- atteindre un consensus au sein d’un groupe ;
un “débat interne” d’une nature similaire.

Ce serait une sorte de transposition de la pratique du mathématicien.

Proofs and refutations. The logic of mathematical discovery
Lakatos, 1976

Des questions de recherche

Quels sont les effets possibles de l’utilisation d’assistants de preuve sur la façon dont les étudiants apprennent la démonstration ?
Quelles caractéristiques des assistants de preuve sont susceptibles de renforcer ou de limiter ces effets ?
Comment affectent-elles l’activité de démonstration ?

L’aspect linguistique de l’interaction

Types de langages

Impératifs: On donne des ordres (appelés tactique) pour construire et compléter la démonstration.
Déclaratifs: La démonstration est une suite d’assertions mathématiques accompagnées de leur justification.

Différents points de vue peuvent mener à différents choix :

Validation pure: Assistants avec langages de tactiques élaborés (Coq, Lean…)
Validation et communication, passage à la preuve écrite: Assistants avec style déclaratif, langage naturel contrôlé (Mizar, Isabelle/Isar, Lean Verbose, Coq Waterproof, Lurch…)
Conceptualisation, conjectures, contre-exemples: HRL (Pease and Colton), QED-Tutrix (Richard) (intelligent tutors for learning)

Mais tout cela reste essentiellement du texte.

Exemple : CoqIDE

L’interface standard de Rocq.

Exemple : Rocq dans VSCode

Une variation sur la précédente, la même preuve avec des commentaires.

Exemple : Lean verbose

Une bibliothèque pour Lean, pour se rapprocher de la langue naturelle.

Exemple avec Deaduction

Une interface à boutons sur Lean, conçue pour enseigner.

Categoriser les effets des assistants de preuve

Les aspects concernés

Mémorisation et formulation
Manipulation d’énoncés formels
Perception de la structure d’un raisonnement
Niveau de langue et précision

Les caractéristiques qui peuvent avoir un effet :

Langage et mode d’interaction: la nature de ce que fournit l’utilisateur, le style impératif ou déclaratif, le nommage des objets, la possibilité d’écrire de énoncés mal formés…
Automatisation et assistance à l’utilisateur: bibliothèques mathématiques, sélection et application de règles logiques, gestion de la portée des variables, enchaînement des inférences et des calculs, nature des rétroactions
Structure des preuves et visualisation des états: point de vue local ou global, statut des énoncés, possibilité de créer des définitions et des lemmes

Observations

Les étudiants parviennent à résoudre plus d’exercices avec les interfaces visuelles à boutons.
Les outils ont tendance à induire des stratégies de tâtonnement et d’essai-erreur.
Le langage naturel contrôlé a un effet sur les productions sur papier des étudiants.
Effet “tunnel” : l’interaction tend à limiter la perception à l’état local de la preuve au détriment de la structure globale.

Proof assistants for undergraduate mathematics and computer science education : elements of a priori analysis.
Bartzia, EB, Meyer & Narboux, ongoing work.

Beaucoup de travaux restent à faire…

projet Inria LiberAbaci — travailler l’utilisabilité de Rocq pour l’enseignement
projet ERC Malinca — traiter les aspects linguistiques et les questions de corpus
projet ANR Appam — analyser les assistants de preuve par les cadres didactiques

En résumé…

On peut calculer pour établir des résultats mathématiques.
On peut élaborer des démonstrations formalisées,
- l’ordinateur aide à les construire,
- il certifie la validité des démonstrations produites.
Cela questionne le processus de validation par la communauté.
Pour enseigner,
- cela peut faire éprouver les règles de raisonnement formelles,
- cela peut aider à structurer des arguments,
- cela ne donne pas d’intuition sur les objets mathématiques.
Il y a un fort présupposé formaliste.
On n’est qu’au début du chemin.

Peut-on faire des démonstrations avec un ordinateur ?

Manifestement, oui

Démontrer avec un ordinateur ?