terence tao offre une récompense au cerveau le plus puissant d'internet ! les humains ia subvertissent les problèmes mathématiques ? les internautes de versailles sont partis
2024-09-29
한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina
nouveau rapport de sagesse
editeur : énée si endormi[introduction à la nouvelle sagesse]récemment, tao zhexuan a lancé un défi à la majorité des internautes et des passionnés de mathématiques : les passionnés de mathématiques populaires, les assistants de preuve, les assistants automatisés et l'ia peuvent-ils unir leurs forces pour prouver des problèmes mathématiques qui s'étendent sur plusieurs ordres de grandeur ?
envie de participer au projet de recherche en mathématiques « crowdsourcing » lancé par terence tao ?l'opportunité est venue !la recherche mathématique sur la preuve assistée par l’ia devient de plus en plus réalisable
chacun d'eux connaît suffisamment certains aspects du projet pour valider les contributions de chacun.mais si l’on souhaite organiser des projets de recherche mathématique à plus grande échelle, notamment des projets impliquant des contributions publiques, c’est beaucoup plus difficile.la raison est qu'il est difficile de vérifier la contribution de chacun.fin 2023, terence tao a annoncé que le projet lean4, qui formalisait la preuve de la conjecture polynomiale de freiman-ruzsa, avait abouti au bout de trois semaines (la photo montre le dernier statut)sachez qu'une seule erreur dans une partie d'un argument mathématique peut entraîner l'échec de l'ensemble du projet.de plus, étant donné la complexité d’un projet mathématique typique, il n’est pas réaliste de s’attendre à ce que les membres du public ayant une formation de premier cycle en mathématiques apportent des contributions significatives.nous pouvons également en déduire que l’intégration d’outils d’ia dans des projets de recherche mathématique est également extrêmement difficile.étant donné que l’ia peut générer des arguments qui semblent raisonnables mais qui n’ont en réalité aucun sens, une vérification supplémentaire est requise avant que la partie générée par l’ia puisse être ajoutée au projet.heureusement, les langages assistés par preuve tels que lean offrent des moyens potentiels de surmonter ces obstacles et permettent la collaboration entre les mathématiciens professionnels, le grand public et les outils d'ia.cette approche repose sur le principe selon lequel les projets peuvent être décomposés de manière modulaire en parties plus petites qui peuvent être réalisées sans avoir à comprendre l'ensemble du projet.les exemples actuels incluent principalement des projets qui formalisent des résultats mathématiques existants (comme la formalisation de la conjecture pfr récemment prouvée par marton).ces formalisations sont principalement réalisées grâce au crowdsourcing par des contributeurs humains (y compris des mathématiciens professionnels et des membres intéressés du public).dans le même temps, des tentatives émergent également visant à introduire des outils plus automatisés pour accomplir cette tâche, notamment des prouveurs de théorèmes automatiques traditionnels et des outils plus modernes basés sur l’ia.il devient possible d'explorer de nouveaux problèmes mathématiques
et,terence taoon pense également que ce nouveau paradigme peut être utilisé non seulement pour formaliser les mathématiques existantes, mais aussi pour explorer des mathématiques complètement nouvelles !dans le passé, lui et son successeur ont organisé un projet de collaboration en ligne « polymath », qui en est un bon exemple.cependant, ce projet n'intégrait pas de langage auxiliaire de preuve dans le flux de travail, et les contributions devaient être gérées et vérifiées par des modérateurs humains, ce qui prenait beaucoup de temps et limitait l'expansion ultérieure de ces projets.maintenant, tao zhexuan espère que l'ajout d'un langage auxiliaire de preuve pourra briser ce goulot d'étranglement.il s'intéresse particulièrement à la possibilité d'utiliser ces outils modernes pour explorer simultanément une classe de problèmes mathématiques, plutôt que de se concentrer sur un ou deux problèmes à la fois.essentiellement, cette approche est modulaire pour les tâches répétitives, et les outils de crowdsourcing et d’automatisation peuvent être particulièrement utiles s’il existe une plateforme pour coordonner rigoureusement toutes les contributions.ce type de problème mathématique n’aurait pas été évolutif avec les méthodes précédentes. à moins que vous n'exploriez lentement un point de données à la fois avec des articles individuels sur plusieurs années jusqu'à ce que vous obteniez une intuition raisonnable sur ce type de problème.de plus, disposer d'un vaste ensemble de données sur les problèmes peut aider à effectuer des évaluations des performances de divers outils d'automatisation et à comparer l'efficacité de différents flux de travail.en juillet de cette année, le cinquième numéro de busy beaver a été confirmé : 47 176 870.certains projets informatiques participatifs antérieurs, tels que great internet mersenne prime search (gimps), sont similaires dans leur esprit à ces projets, bien qu'ils utilisent un mécanisme de preuve de travail plus traditionnel, plutôt que de prouver un langage auxiliaire.terence tao a déclaré qu'il serait intéressé de savoir s'il existe d'autres exemples de projets de crowdsourcing explorant des espaces mathématiques, et s'il y a des leçons apprises qui peuvent être utilisées.tao zhexuan propose de nouveaux projets
à cette fin, tao lui-même a proposé un projet visant à tester davantage ce paradigme.ce projet a été inspiré par la question mathoverflow de l'année dernière.peu de temps après, tao zhexuan en a discuté davantage sur son mathstodon.ce problème appartient au domaine de l'algèbre universelle et implique une exploration à moyenne échelle de la théorie des équations simples du groupe d'origine (magma).le groupe d'origine est un groupe équipé d'opérations binairesl'ensemble g.initialement, cette opération n'est associée à aucun axiome supplémentaire, le groupe d'origine lui-même est donc une structure relativement simple.bien entendu, en ajoutant des axiomes supplémentaires, tels que des axiomes d’identité ou des axiomes d’associativité, nous pouvons obtenir des objets mathématiques plus familiers tels que des groupes, des semi-groupes ou des monoïdes.nous nous intéressons ici aux axiomes (libres de constantes) d’égalité. ces axiomes concernent l'égalité des expressions construites à partir des opérations o et d'une ou plusieurs inconnues dans g.deux exemples familiers de tels axiomes sont la loi commutative xoy = yox et la loi associative (xoy) oz = xo (yoz).où x, y, z sont des variables inconnues dans le groupe d'origine g.d'un autre côté, l'axiome d'identité (à gauche) eox = x n'est pas considéré ici comme un axiome équationnel car il implique une constante e ∈ g. de tels axiomes impliquant des constantes ne sont pas discutés dans cette étude.ensuite, afin d'illustrer le projet de recherche qu'il a initié, terence tao a présenté onze exemples d'axiomes d'égalité concernant les groupes primitifs.ces axiomes d'égalité sont des équations impliquant uniquement des opérations de groupe primitives et des variables inconnues :ainsi, par exemple, l'équation 7 représente l'axiome commutatif, tandis que l'équation 10 représente l'axiome associatif.l'axiome constant équation 1 est le plus fort, car il restreint le groupe original g à avoir au plus un élément ; au contraire, l'axiome réflexif équation 11 est le plus faible, et tous les groupes originaux satisfont à cet axiome ;ensuite, nous pouvons explorer la relation de dérivation entre ces axiomes : quels axiomes peuvent déduire quels axiomes ?par exemple, l’équation 1 mène à tous les autres axiomes de cette liste, qui à leur tour mènent à l’équation 11.l’équation 8 peut être utilisée comme cas particulier pour dériver l’équation 9, qui à son tour peut être utilisée comme cas particulier pour dériver l’équation 10.la relation de dérivation complète entre ces axiomes peut être décrite par le diagramme de hasse suivant :ce résultat répond spécifiquement à une question du site web de questions-réponses sur les mathématiques mathoverflow : existe-t-il des axiomes équationnels entre l'axiome constant (équation 1) et l'axiome d'associativité (équation 10).il convient de noter que la plupart des relations d’implication ici sont faciles à prouver. il existe cependant une relation d’implication non triviale.cette relation a été trouvée dans une réponse à un article de mathoverflow étroitement lié à la question précédente :proposition 1 : l'équation 4 implique l'équation 7preuve : supposons que g satisfasse l’équation 4, donccela est valable pour tout x,y ∈ g.en particulier, lorsque y = xox, il s'ensuit que (xox) o (xox) = (xox) ox.en appliquant à nouveau (1), nous pouvons conclure que xox est idempotent :maintenant, en remplaçant x par xox dans (1) et en utilisant (2), nous obtenons (xox) oy = yo (xox).en particulier, xox et yoy sont interchangeables :de plus, en appliquant (1) deux fois, on obtient (xox) o (yoy) = (yoy) ox = xoy.par conséquent, (3) peut être simplifié en xoy = yox, ce qui correspond à l’équation 7.la formalisation du processus d’argumentation ci-dessus peut être trouvée dans le lean.il convient toutefois de noter que la question générale de savoir si un ensemble d’axiomes d’égalité détermine un autre ensemble d’axiomes d’égalité est indécidable.la situation ici est donc quelque peu similaire au défi "busy beaver", c'est-à-dire qu'après un certain point de complexité, nous sommes forcément confrontés à des problèmes indécidables, mais avant d'atteindre ce seuil, nous espérons encore découvrir des problèmes et des phénomènes intéressants.le diagramme de hass ci-dessus affirme non seulement les relations d'implication entre les axiomes d'égalité répertoriés, mais affirme également les relations de non-implication entre les axiomes.par exemple, comme le montre la figure, l'axiome commutatif équation 7 n'implique pas l'axiome de l'équation 4 (x + x) + y = y + x.pour le prouver, il suffit de trouver un exemple de groupe primitif qui satisfait l’axiome commutatif équation 7 mais ne satisfait pas l’axiome équation 4.par exemple, dans ce cas, on peut choisir l’ensemble d’entiers naturels n, dont l’opération est xoy := x+y.plus généralement, le diagramme affirme les relations de non-implication suivantes, qui (avec les relations d'implication déjà notées) décrivent complètement l'ensemble partiellement ordonné des relations d'implication entre ces onze axiomes :ici, tao zhexuan invite les lecteurs à proposer des contre-exemples pour compléter certaines preuves.le contre-exemple le plus difficile à trouver est que l’équation 9 ne peut pas déduire l’équation 8.une solution peut être apportée en utilisant le lean.de plus, tao zhexuan fournit également un référentiel github qui contient des preuves lean de toutes les relations d'inclusion et d'anti-inclusion ci-dessus.on voit que le simple calcul du diagramme de haas à 11 équations est déjà un peu fastidieux.le projet proposé par terence tao est une tentative d'étendre ce diagramme de hass de plusieurs ordres de grandeur pour couvrir un plus large éventail d'ensembles d'équations.l'ensemble qu'il a proposé était ε, l'ensemble d'équations utilisant l'opération de groupe originale o au plus quatre fois, jusqu'à ce que les axiomes de réflexivité et de symétrie des équations de somme soient réétiquetés.cela inclut les onze équations mentionnées ci-dessus, mais il y en a bien d’autres.combien y en a-t-il encore ?rappelons que le nombre catalan c_n est le nombre de façons de former une expression en utilisant l'opération binaire o (appliquée à n+1 variables d'espace réservé) ; et étant donné une chaîne de m variables d'espace réservé, le nombre de bell b_m est le nombre de façons dont ces variables sont noms attribués (qui peuvent être réétiquetés), ce qui permet d'attribuer le même nom à certains espaces réservés.par conséquent, en ignorant la symétrie, le nombre d’équations impliquant au plus quatre opérations estle nombre d'équations dont les côtés gauche et droit sont identiques estceux-ci sont équivalents aux axiomes réflexifs (équation 11).les 9 118 équations restantes apparaissent par paires en raison de la symétrie des équations, donc la taille totale de ε est
tao zhexuan a déclaré qu'il n'avait pas encore généré une liste complète de ces identités, mais il soupçonne que cela peut être facilement réalisé en utilisant python.à l’aide d’outils d’ia, vous devriez être en mesure de générer la plupart du code requis.il a dit qu’il n’avait aucune idée à quoi ressemblerait la géométrie de ε.la plupart des équations seront-elles incomparables les unes aux autres ? sera-t-il divisé en axiomes « forts » et axiomes « faibles » ?désormais, la zone de message de terence tao contient des dizaines de commentaires.lecteurs intéressés, tao zhexuan vous a également adressé une invitation.
