Yang-Mills : les physiciens refusent de publier trop tôt la preuve d’OpenAI
Un modèle d’OpenAI a produit 1 147 pages de preuve sur Yang-Mills. Cinq physiciens la vérifient avant publication, et même validée, elle resterait partielle.
Une preuve de 1 147 pages, produite par un modèle d’OpenAI, sur l’un des grands chantiers de la physique théorique. Pourtant, selon Numerama, les physiciens chargés de l’examiner refusent de la publier avant d’avoir confirmé qu’elle tient. Quand une IA prétend démontrer, qui a le dernier mot ?
Ce qu’OpenAI a présenté
Une annonce spectaculaire est-elle un fait établi ou une promesse ? Ici, c’est une promesse non validée, et Numerama le dit sans détour.
La théorie de Yang-Mills décrit les forces qui agissent entre les particules. Ses fondations mathématiques restent à démontrer : il s’agit de prouver, avec la rigueur des mathématiciens, que cette théorie existe vraiment en tant qu’objet cohérent.
Selon Numerama, un modèle d’OpenAI a produit une preuve de 1 147 pages liée à cette question. C’est un document très long, et le média parle d’une complexité « redoutable ». Relire un tel texte ligne par ligne est un travail de longue haleine, pour n’importe quel spécialiste.
D’autres articles de Numerama signalent une polémique autour de cette preuve. L’un indique qu’OpenAI affirme avoir résolu l’une des plus grandes énigmes de la physique, « mais garde la preuve secrète ». Ces intitulés suggèrent un désaccord sur la diffusion du texte. Les circonstances exactes ne sont pas détaillées dans l’article que nous citons.
Cinq physiciens, et un refus de se précipiter
Sur quoi repose la confiance dans un résultat scientifique ? Sur des spécialistes qui ont relu et qui engagent leur nom. Une démonstration que personne n’a contrôlée n’est, pour la science, qu’un document.
D’après Numerama, cinq physiciens sont chargés d’examiner cette preuve. Ils refusent de la publier avant d’avoir confirmé sa justesse. Leur méthode tient en deux temps : vérifier d’abord sa formalisation dans Lean, puis soumettre leur analyse à la communauté scientifique.
Cette prudence n’est pas partagée par tous. Un autre titre du média rapporte que des mathématiciens s’agacent : il n’y aurait, selon eux, « aucune raison scientifique de retarder » la preuve. Numerama évoque un appel de mathématiciens, auquel les physiciens ne cèdent pas.
Les deux positions se comprennent. D’un côté, rendre le texte public permettrait à beaucoup de chercheurs de le lire en parallèle. De l’autre, diffuser plus de mille pages sans savoir si elles sont justes peut propager une erreur, ou une fausse victoire. Rien ne permet de trancher à ce stade, et cet article ne le fait pas.
Lean, le correcteur qui ne se fatigue pas
Comment s’assurer qu’un texte aussi long ne cache pas une faille à la page 800 ? C’est la question à laquelle répond le choix de Lean.
Lean est un logiciel de vérification de preuves mathématiques. On y traduit chaque raisonnement dans un langage très strict, et le programme contrôle étape par étape que chaque déduction est valide. Cette traduction s’appelle la formalisation. Numerama ne détaille pas le fonctionnement de Lean ; cette description est un repère général sur ce type d’outil.
En clair : c’est un correcteur d’orthographe, mais pour le raisonnement. Si une étape est bancale, le logiciel la signale.
Ce choix de méthode a probablement un coût en temps : traduire plus de mille pages dans un langage aussi strict ne se fait pas en un après-midi. Numerama ne donne aucun calendrier, et nous ne pouvons pas en annoncer un. Ce que la source établit, c’est l’ordre des opérations : d’abord la vérification dans Lean, ensuite seulement l’analyse soumise à la communauté.
Même validée, une partie seulement du problème
Il faut éviter de confondre « percée » et « problème résolu ». Numerama est net sur ce point : même confirmée, la démonstration ne couvrirait que l’existence de la théorie de Yang-Mills.
Elle ne résoudrait pas, précise le média, le problème de l’écart de masse, qui est nécessaire pour décrocher le prix du millénaire. Numerama n’explique pas ces deux notions plus avant dans l’article cité, et nous ne les détaillerons pas au-delà de ce qu’il écrit. Retenons l’essentiel : il resterait une étape distincte, et non des moindres, avant d’arriver à ce prix.
Autrement dit, l’annonce, si elle se confirme, serait un morceau, pas le tout. Le titre qui évoque « l’une des plus grandes énigmes de la physique » doit donc se lire avec cette réserve. Écrire qu’une IA a « résolu » le problème du prix du millénaire irait plus loin que ce que rapporte la source.
Qui a le dernier mot ?
La place de l’IA dans la recherche dépend d’une question simple : qui contrôle ce qu’elle produit ?
La réponse que dessine cet épisode est sobre. Le dernier mot ne revient ni à l’entreprise qui annonce, ni à la machine qui produit. Il revient à la communauté qui vérifie. Ici, cela passe par un logiciel de contrôle strict, puis par des experts qui engagent leur réputation.
La prudence des physiciens n’est donc pas forcément un frein à l’innovation. Elle est la condition pour qu’un résultat compte. Une IA peut produire des centaines de pages en peu de temps. Mais produire n’est pas démontrer : tant que personne n’a contrôlé, le texte reste une hypothèse.
Plusieurs questions restent ouvertes, et rien de public n’y répond à ce stade. La preuve sera-t-elle publiée, et quand ? La formalisation dans Lean aboutira-t-elle ? Et si la preuve est confirmée, comment crédite-t-on un résultat obtenu par un modèle ? Le verdict des cinq physiciens, quand il viendra, vaudra plus que n’importe quelle annonce.
Sources
Pour aller plus loin Dossier : Quelle IA choisir ?
