Dix agents formalisent une preuve du problème de Thomson

OOndine

Vals AI affirme que 10 agents Claude Sonnet 5.5 ont produit en environ 15 heures une preuve formelle du problème de Thomson pour 7 points sur une sphère, selon AlphaSignal. Pour ce cas précis, la démonstration établit que la bipyramide pentagonale est l’unique configuration minimale, en considérant comme équivalentes les configurations obtenues par rotations, réflexions ou permutations des points. Le résultat porte donc sur 7 points et sur cette configuration minimale, et non sur une affirmation générale concernant toutes les tailles du problème de Thomson. La preuve est encodée dans un fichier Lean de 17 895 lignes ; elle a été vérifiée par Lean, puis contrôlée par un noyau indépendant, nanoda. Ce noyau a accepté 47 854 déclarations, un contrôle qui concerne les éléments formels soumis à vérification et qui s’ajoute à celui réalisé par Lean. La démonstration combine des bornes issues de la programmation semi-définie, des certificats exacts, de l’arithmétique par intervalles et une analyse de minimalité locale ; ces différentes méthodes participent à la construction de la preuve. Vals AI indique que les sources et les scripts de vérification sont publiés sur GitHub, afin que le travail formalisé et les contrôles associés puissent être examinés, tandis que ce résultat illustre une utilisation d’agents d’intelligence artificielle pour produire une démonstration mathématique soumise à des vérifications informatiques.