d'ici 2027, nous ne serons pas du tout proches d'avoir formalisé juste quelques % de ce à quoi les mathématiques ressemblaient avant la preuve de Wiles du dernier théorème de Fermat. Nous n'aurons également pas d'IA réalisant des recherches mathématiques nouvelles et réelles d'ici 2035 (la plupart des ensembles de problèmes d'Erdős et de l'IMO n'ont rien à voir avec cela) sans que l'ensemble du point et de la difficulté (qui est de comprendre ce qui compte réellement et d'être véritablement créatif) - cela n'accélérera que les parties que les humains ne se soucient que très peu (la partie formelle). La recherche mathématique consiste autant à identifier quelles sont les bonnes questions, ce qui est intéressant par rapport à ce qui est trivial et peut-être surtout à comprendre réellement pourquoi un résultat est important (!!!) que tout autre chose. Cela ne mentionne pas non plus que toutes les zones des mathématiques n'ont pas les mêmes "accessibilités" computationnelles. Nous sommes encore très loin (mais nous sommes plus proches !) de voir la recherche, en particulier la recherche mathématique, être "dirigée" par l'IA et quiconque vous dit le contraire signifie soit par là "une définition incroyablement ennuyeuse de la recherche", soit ment, soit est un idiot, soit les trois. Je pense que l'idée que la moitié des nouveaux résultats mathématiques soient générés par l'IA d'ici 2027 est hilarante, à moins que nous ne soyons d'une manière ou d'une autre mentalement incapables de définir un résultat mathématique comme juste une chaîne formelle de symboles et de déductions logiques basées sur quelques règles simples. Pour être clair, mon point n'est pas que "l'autoformalisation" des mathématiques n'est pas valide, elle est très précieuse pour de nombreuses raisons - principalement parce que les humains feront de meilleures mathématiques et/ou utiliseront mieux leur temps, mais certainement cela n'a aucune valeur en soi et donc ne "automatise pas la recherche mathématique". Mon point n'est pas non plus que l'IA ne pourra jamais faire de véritables recherches mathématiques : je crois qu'elle le peut, mais certainement cela ne découlera pas de la technologie actuelle de 2020-2025 dans deux ans.

les vrais gars des maths peuvent se lever et être en désaccord, je ne suis pas un vrai gars des maths, mais je doute qu'un pur gobelin informatique ou un pur gobelin des maths puisse vraiment être en désaccord car ils ne connaissent tout simplement pas assez les deux côtés.

Pour être clair, je pense que nous sommes actuellement à l'ère où l'IA peut fournir des preuves novatrices lorsqu'elle est associée aux humains, et l'autoformatisation continuera de croître, et GDM obtiendra probablement Navier-Stokes bientôt, etc. Mon propos n'est pas qu'elle n'est pas utile, juste que la partie fondamentale la plus difficile est toujours et sera toujours pilotée par l'humain jusqu'à ce qu'il y ait des avancées significatives dans la recherche en IA (en dehors de la folie des modèles autoregressifs uniquement basés sur le décodeur que nous avons et que nous aurons encore pendant des années).

@nasqret J'ai spécifiquement aussi restreint mon propos à "la pile technologique actuelle" qui est composée de décodeurs auto-régressifs uniquement + 10000 choses collées ou boulonnées, et à ma connaissance, il n'y a rien de vraiment en train de se préparer qui pourrait être commodifié d'ici 2027 (ou 2030) pour rendre cela possible.