Contexte historique

Au début du XXᵉ siècle, David Hilbert a proposé un programme d’axiomes complet et cohérent pour fonder les mathématiques. En 1931, Kurt Gödel a démontré l’impossibilité de ce projet avec ses théorèmes d’incomplétude, montrant qu’aucun système suffisamment puissant ne peut être à la fois complet et cohérent. Deux ans plus tard, Alan Turing a prouvé l’indécidabilité du problème d’arrêt, établissant que l’existence d’un algorithme décisif pour toutes les propositions mathématiques est impossible. Ces résultats ont pourtant posé les bases de l’informatique théorique.

Mécanismes de preuve assistée

Les assistants de preuve modernes, comme Lean, reposent sur la théorie des types dépendants, une évolution de la théorie des types de Russell. Cette architecture encode chaque proposition comme un type et chaque preuve comme un terme de ce type, conformément à la correspondance de Curry‑Howard. Ainsi, vérifier une preuve revient à vérifier la typabilité d’un programme. Exemple minimal :

theorem add_comm (a b : Nat) : a + b = b + a :=
  Nat.add_comm a b

Le code ci‑dessus est à la fois une preuve formelle et un programme exécutable dans l’interpréteur Lean.

Rôle des IA dans la génération de preuves

Des modèles d’IA, notamment les large language models entraînés sur des bases de code et de mathématiques, peuvent proposer des scripts Lean complets. Des expériences récentes (par ex. GPT‑f ou AlphaMath) ont généré des preuves de théorèmes de niveau intermédiaire sans intervention humaine, puis ont été vérifiées automatiquement par le noyau Lean. Cette capacité réalise, en pratique, l’« machine à prouver » envisagée par Hilbert, bien que la validation repose toujours sur le moteur de vérification.

Implications pour la pratique informatique

Le texte souligne que la confiance aveugle dans du code ou une preuve générée par IA, sans lecture humaine, constitue un risque. En informatique, la lecture du code source reste le moyen d’assurer la compréhension du comportement d’un programme, même lorsqu’il est formellement vérifié. Le parallèle avec les mathématiques est explicite : lorsqu’une preuve IA est trop longue, les mathématiciens la simplifient pour la rendre lisible, appliquant des abstractions et des refactorisations. De même, les développeurs doivent adopter des langages de plus haut niveau, des abstractions et des revues de code pour garder le contrôle sur les systèmes automatisés. Le danger évoqué – déléguer la compréhension à la machine – rappelle les incidents où des diagnostics médicaux basés sur l’IA ont entraîné des erreurs graves, soulignant l’importance de la transparence et de la vérifiabilité.