Pour la première fois, un système basé sur l’IA conçu pour vérifier des preuves mathématiques a identifié une erreur fondamentale dans un article de physique évalué par des pairs. La découverte, faite par Joseph Tooby-Smith de l’Université de Bath, met en évidence une préoccupation croissante : combien d’erreurs similaires peuvent exister dans la littérature scientifique existante ? Cet événement souligne le potentiel des outils de vérification automatisés pour remodeler la publication universitaire et améliorer la fiabilité des découvertes scientifiques.
L’essor de la vérification formelle
La vérification formelle – le processus de vérification rigoureuse de la cohérence mathématique et logique – est de plus en plus courante en mathématiques. Des logiciels spécialisés, comme le langage Lean utilisé dans ce cas, peuvent identifier les contradictions et les lacunes dans les preuves qui pourraient passer inaperçues lors d’un examen humain. Cette approche ne consiste pas seulement à détecter les erreurs ; cela est considéré comme un moyen de résoudre des problèmes notoirement difficiles, tels que la conjecture ABC non résolue, pour laquelle même les experts ne sont pas d’accord sur la validité des solutions proposées.
La physique au microscope
Tooby-Smith a appliqué la vérification formelle à un article de 2006 sur la stabilité du potentiel du modèle à deux doublets de Higgs (2HDM), un ouvrage largement cité en physique des particules. L’objectif était d’intégrer l’article dans PhysLib, un projet visant à créer une base de données formalisée de recherche en physique sur le modèle du succès MathsLib pour les mathématiques. L’IA a révélé qu’une condition clé présentée dans l’article original ne garantissait pas une solution stable, comme le prétendaient les auteurs.
Cette découverte n’était pas une tentative délibérée de discréditer l’œuvre. Comme l’explique Tooby-Smith, l’équipe visait un « exercice de cases à cocher » pour construire une bibliothèque fiable de physique formalisée. Cependant, l’erreur découverte soulève une question cruciale : si un article bien cité pouvait contenir un tel défaut, combien d’autres pourraient être également défectueux ?
Pourquoi c’est important
La physique repose sur la rigueur mathématique, mais les physiciens donnent souvent la priorité aux résultats plutôt qu’aux détails exhaustifs. Contrairement aux mathématiciens, qui fournissent généralement des étapes de preuve explicites, les physiciens peuvent omettre des détails apparemment mineurs qui, comme le montre ce cas, peuvent miner la validité d’un théorème. Cette différence de pratique signifie que les articles de physique sont potentiellement plus vulnérables aux erreurs non examinées.
L’avenir de la validation scientifique
Les implications de cette découverte sont importantes. Même s’il est peu probable que cette erreur invalide les travaux en aval qui ont cité l’article (un erratum est déjà en cours), elle renforce l’argument en faveur de l’intégration de la vérification formelle dans le processus de publication standard.
Kevin Buzzard, de l’Imperial College de Londres, note que la formalisation a déjà transformé les mathématiques et qu’il n’y a aucune raison pour que la physique théorique ne puisse pas bénéficier de la même approche. Le défi réside cependant dans la constitution d’un corpus suffisamment vaste de données physiques formalisées pour entraîner efficacement les modèles d’IA. “Idéalement, nous avons besoin d’un million de lignes de physique… si les machines ne sont pas très douées pour faire de la physique au début, alors il y aura du travail manuel au début”, explique Buzzard.
La vérification automatisée est sur le point de devenir un outil essentiel pour garantir l’exactitude scientifique. Même si l’effort initial peut demander beaucoup de travail, les avantages à long terme d’un dossier scientifique plus fiable sont indéniables.
