Une IA peut-elle assister la recherche de preuves de conjectures difficiles?

Peut-être que l'outil Draft, Sketch, Prove, en ce qui concerne Goldbach, pourrait être utilisé pour prouver que l'algorithme de réduction de rang dont je parle (en anglais principalement) sur mathstodon comporte $O(\log^{C}n)$ étapes.

Ça ne répond pas directement à la question mais l'IA dans les maths et la formalisation sont en cours.
Concernant les assistants de preuve, les dernières actualités et avancées mettent toujours en avant Lean, avec Scholze qui formalise ses preuves, Kevin Buzzard qui est extrêmement actif et qui vient d'obtenir une bourse de presque 1000000£ pour formaliser le dernier théorème de Fermat sur 5 ans, la bibliothèque mathématique mathlib...
Et récemment un laboratoire d'IA, Morph, a sorti Moogle, un moteur de recherche sémantique pour Mathlib. On peut désormais trouver des théorèmes en utilisant le langage naturel. Ils ambitionnent aussi de faire un "personal AI proof engineer" même si pour le moment je me demande ce que ça va être exactement.

Bonjour, ce n'est pas parce qu'un ordinateur est impliqué qu'il y a forcément de l'IA derrière.
Sinon dans l'application de l'IA, il y a des travaux sur l'approximation numérique des solutions des EDP , ou EDP stochastique par des réseaux de neurones. 
Je ne suis pas spécialiste mais je pense qu'il faut plus interpréter ça comme un "nouveau" type de schéma numérique plutôt qu'autre chose, d'ailleurs il me semble que ça s'appelle les "deep schemes" (schéma profond). Un des avantages de cette approche c'est le temps de calcul, une fois le réseau entrainé (ce qui peut prendre un certain temps), le calcul d'une solution numérique peut être plus rapide que pour les schémas numériques classiques.
On peut aussi relier ça avec les théorèmes d'approximations universelles des réseaux de neurones par exemple sans rentrer dans les détails : l'ensemble des réseaux de neurones à une couche sont denses dans l'ensemble fonctions continues,  (l'approximation de fonction étant importante dans le domaine des EDP, dans mes souvenirs les preuves de ces théorèmes sont des preuves  qui réutilisent les techniques d'analyse fonctionnelle). 
Pour un peu plus de détail : https://fr.wikipedia.org/wiki/Théorème_d'approximation_universelle

Remarque : Ce ne sont pas des méthodes miracles, la densité fournit l'existence d'un réseau aussi proche d'une fonction qu'on veut mais si la preuve de l'existence n'est pas constructive ça peut être très compliqué de trouver les paramètres du réseau qui approche "la fonction cible", il y a quand même un bon point les réseaux de neurones sont des fonctions "facile" à construire dans la pratique.

@Soc: J'ai bien peur qu'une IA d'aujourd'hui soit bien incapable de produire une démonstration d'un théorème non encore prouvé par un être humain (un "vrai" théorème qui apparaît "naturellement" dans la vie d'un mathématicien professionnel) pour la raison que la démonstration en question ne ressemblera sans aucun doute à rien qui a été fait précédemment.
Par ailleurs, une IA pour chercher des patterns doit bien calibrer cette recherche, en fait, une démonstration nouvelle serait contenue, en quelque sorte, dans la requête construite.

Non. Regarde les vidéos, ils expliquent assez bien.

@Soc: Pour ce que je comprends de l'IA à la chatGPT: A la suite de calculs longs sur une gigantesque base de données* (qui peuvent être des images, du texte...) on a identifié des patterns.
Une requête consiste à demander à une IA de rechercher si une expression n'est pas un bout d'un pattern et dans le cas où l'IA connaît ce pattern elle va te donner le pattern complet.
*: qui n'existerait pas sans internet. Internet agrège du contenu fabriqué par des millions de gens.

Voilà une description plus  précise (tiré de l’ouvrage, « Machine learning », de Kevin P. Murphy)

@AlainLyon: Les IA qui produisent du texte dans une langue ont digéré tout Wikipedia qui est une encyclopédie produite surtout par des bénévoles.

@AlainLyon: Je ne suis pas retraité et j'ai produit un peu de contenu pour Wikipedia (un très modeste contenu), il me semble difficile d'affirmer que Wikipedia repose seulement sur le travail de retraités.

Lost in translation?

Puisque la discussion tourne autour d'une fausse démonstration, je l'ai déplacée vers Shtam.
Par curiosité j'ai aussi posé une question à Chat GPT :
Moi : peux-tu me démontrer que tout entier pair supérieur ou égal à 4 est la somme de deux nombres premiers ?
ChatGPT : La conjecture selon laquelle tout entier pair supérieur ou égal à 4 peut être exprimé comme la somme de deux nombres premiers est connue sous le nom de conjecture de Goldbach. Malheureusement, à ce jour, elle n'a pas été démontrée de manière générale. Bien que cette conjecture soit largement acceptée et vérifiée empiriquement pour de nombreux nombres, une démonstration formelle et générale n'a pas encore été trouvée.

La méthode de ChatGPT: plutôt que de vous enfumer, maintenant il utilise une technique éprouvée: quand vous avez fini de lire ce qu'il a répondu, vous ne comprenez plus votre question.

Pour rajouter un jeton au jukebox, les IA du type GPT étant des transformers (donc des encodeurs très sophistiqués), elles ne permettront jamais toutes seules de généraliser très loin de leurs données d'entrainement. De manière plus générale, les IA "actuelles" ne font que des interpolations en regardant les données d'entrainement les plus proches de l'entrée dans une certaine métrique qui est apprise lors de l'entrainement (ça a été prouvé théoriquement et ça se vérifie en pratique).

Les réseaux de neurones supervisés sont utilisés (avec un certain succès) en théorie des cordes. On travaille sur des surfaces projectives qui sont le lieux des zéros de polynômes homogènes de degré $k$. Il semble difficile de trouver des expressions exactes de certaines structures locales définies sur ces surfaces. Il existe bien des algorithmes qui fournissent des approximations mais ils deviennent vite très coûteux en calculs. L’idée est de les court-circuiter en demandant à un réseau de neurones de « faire des prévisions » à partir d’un ensemble d’entraînement constitué de quelques milliers de points pris au hasard sur une variété projective. Mais pour chacun de ces points, (et c’est là que ça se complique sacrément !) il y a la valeur du déterminant d’une certaine métrique.  Les prévisions de l’IA portent sur le « comportement » de ce déterminant quand on augmente un paramètre.

Bref ! J’ai attaché deux extraits dignes de foi, c’est plus prudent… En théorie des cordes, le « machine learning » est utile pour faire des calculs numériques plus précis et beaucoup moins longs (de plusieurs années parfois !) sur des variétés compliquées et qui peuvent avoir un nombre extravagant de dimensions. On n’est pas vraiment dans la « résolution de conjectures » à proprement parler mais plus dans l’expérimentation numérique.

Je ne suis pas d’accord avec le qualificatif de « perroquet «  concernant les IA. D’abord, il a été démontré que les perroquets et les corvidés possèdent des notions de probabilités. Ensuite, quand on demande à une IA de « prédire » la valeur d’un déterminant ou de déterminer la sous-espèce de l’orchidée sur la photo, on lui demande de trouver une relation fonctionnelle (la plus probable ) entre une valeur d’entrée $x_i$ et une valeur (connue) de sortie $y_i$, le couple $(x_i,y_i)$ étant un élément de l’ensemble d’entraînement. Il me semble qu’on n’est plus dans la simple exécution d’un programme.