La faille dans l’article de Tao Zhexuan a été découverte par l’IA, et la prédiction de 26 ans se réalisera ! Devinant la direction de la recherche en regardant le nom du théorème, le grand dieu a qualifié la capacité de l’IA d’incroyable

Source de l’article : New Zhiyuan

Récemment, Tao Zhexuan, un dieu des mathématiques qui souhaite utiliser GPT-4 et Copilot pour faire des recherches, a découvert un bug caché dans son article avec l’aide de l’IA !

Tao Zhexuan a déclaré que dans le processus de formalisation de l’argument de la page 6 avec Lean4, il a constaté que les expressions

À n = 3 et k = 2, elle est en fait divergente.

Ce bug pas si évident a été détecté à temps grâce à Lean4.

La raison en est que Lean lui a demandé de construire 02. Par conséquent, le Lean ne peut pas être basé sur un 0 négatif

Heureusement, il ne s’agit que d’un bogue mineur qui n’existe que lorsque la valeur n est petite. À ce stade, il vous suffit de modifier quelques constantes dans l’article.

Certains fans passionnés de mathématiques se sont exclamés dans cet article : C’est incroyable, et c’est formidable de voir la propagation des assistants de preuve d’IA, jetant une base plus solide pour l’avenir de la recherche mathématique.

Tao Zhexuan a dit que c’est tout à fait possible.

Peut-être que dans un avenir proche, nous pourrons construire une couche d’IA au-dessus du Lean.
En décrivant les étapes de la preuve à l’IA, l’IA peut utiliser le Lean pour exécuter la preuve et, ce faisant, elle peut également faire appel à divers progiciels d’algèbre informatique.

En juin de cette année, Tao Zhexuan a prédit dans un blog sur l’expérience de l’essai GPT-4 -

En 2026, l’IA sera combinée à des outils de recherche et de mathématiques symboliques pour devenir un co-auteur de confiance dans la recherche mathématique.

Pendant cette période, il y a des gens qui continuent à le prouver. Par exemple, des chercheurs de Caltech, de NVIDIA, du MIT et d’autres institutions ont construit un prouveur de théorème basé sur le LLM open-source.

Et Tao Zhexuan l’a également pratiqué, et le nouvel article a commencé à être écrit en GPT-4, et s’est exclamé à plusieurs reprises - la capacité étonnante de GitHub Copilot me met mal à l’aise !

AI Bénédiction Dieu Recherche en mathématiques

Récemment, Tao Zhexuan est complètement « entré dans le gouffre » de l’IA.

Avec l’aide de GPT-4, il a commencé à apprendre à écrire des articles et à faire de la recherche mathématique avec Lean4.

Il était tellement enthousiasmé par le processus qu’il a posté sur Mastodon toutes les quelques heures pour enregistrer ses apprentissages et ses expériences.

En rédigeant un article sur l’inégalité de McLaughlin, Tao a fait un usage intensif d’outils d’IA tels que GPT-4, Copilot et Lean4.

Adresse:

Au fur et à mesure que nous avançons, Tao a terminé la réparation de l’argument de la section 2 de l’article de Lean4.

Cependant, le processus était beaucoup plus fastidieux qu’il ne le pensait, et chaque ligne de preuve prenait environ une heure à formaliser.

Au cours de la première semaine du projet, son goulot d’étranglement était son manque de familiarité avec la syntaxe et les outils Lean ; Mais le goulot d’étranglement actuel réside dans les outils eux-mêmes, qui ne sont pas aussi avancés que ceux des progiciels d’algèbre informatique.

Par exemple, dans une ligne de son article, il affirme que l’inégalité :

Peut être réarrangé comme suit :

En supposant que tous les dénominateurs sont positifs, il s’agit d’une tâche très rapide pour les calculs manuels et peut être effectuée assez facilement dans n’importe quel logiciel d’algèbre informatique standard.

Lean dispose d’outils automatiques très utiles pour gérer les opérations linéaires, mais il n’existe actuellement aucun outil permettant de simplifier automatiquement les expressions complexes impliquant des exposants.

Par conséquent, nous devons traiter la loi exponentielle et d’autres opérations mentionnées ci-dessus étape par étape, et ce processus prend beaucoup de temps.

En fin de compte, Tao décida de ne pas utiliser la notation asymptotique dans cette partie de l’argument, mais d’établir une inégalité avec une constante définie C :

dans lequel

Au départ, Tao pensait qu’il serait « plus simple » de prouver les inégalités avec des valeurs telles que C=7. Cependant, il était fastidieux d’utiliser les outils existants pour prouver rigoureusement C≤7, de sorte que l’idée a été abandonnée au profit d’une valeur C plus formellement opérationnelle. Maintenant sélectionné, la valeur est d’environ 6,16.

À cet égard, certains internautes curieux ont demandé : « Comment l’IA fait-elle pour prouver la vitesse par rapport à l’arithmétique des mains ? »

Tao Zhexuan a déclaré que, sur la base de ses propres observations, les types de tâches qui sont mécaniques pour les progiciels d’algèbre informatique et les calculatrices ne sont pas nécessairement mécaniques pour les assistants de preuve formelle.

Mais avec l’avènement des LLM, nous devrions être en mesure d’unifier tous les outils assistés par ordinateur en un seul outil convivial et universel. Et cet outil aura tous les avantages de chaque composant.

Même, dans un avenir proche, nous pouvons également envisager de construire une couche d’IA au-dessus du Lean -

Les étapes de la preuve sont décrites à l’IA en « anglais mathématique », et l’IA peut ensuite essayer de l’exécuter à l’aide du Lean, en invoquant peut-être un package d’algèbre informatique dans le processus.

Copilot peut deviner les prochaines étapes

Auparavant, dans cet article sur les recherches de McLaughlin sur les inégalités, Tao Zhexuan a été surpris de constater que Copilot était capable de prédire ce qu’il voulait faire ensuite !

Non seulement il peut prédire correctement les multiples lignes de code utilisées pour diverses vérifications de routine, mais il peut également déduire dans quelle direction il veut faire ses recherches en se basant sur le nom du théorème fourni par Tao Zhexuan.

Cela a fait que Tao Zhexuan s’est exclamé encore et encore : C’est incroyable !

Dans le processus de démonstration du théorème 1.3 dans l’article, Tao Zhexuan a utilisé Lean4 pour compléter la formalisation de la preuve du théorème.

Dans l’article, il n’y a qu’une seule page dans le processus de preuve, mais la preuve formelle utilise 200 lignes de Lean4.

Par exemple, dans l’article, Tao Zhexuan ne fait que supposer

est convexe sur tout nombre réel de a>0 et l’inégalité de Jensen est appelée par la suite. Mais le code prend environ 50 lignes.

Au cours de ce processus, GitHub Copilot a montré toutes sortes de prédictions divines et a prédit comme par magie la prochaine direction des recherches de Tao Zhexuan.

La stratégie de réécriture de Lean lui permet de réviser des hypothèses ou des objectifs à long terme grâce à des substitutions ciblées.

Cette fonctionnalité est extrêmement importante car elle permet aux gens de manipuler librement ces expressions sans avoir à les saisir dans leur intégralité tout le temps.

Comparativement, en LaTex, cette opération est beaucoup plus lourde.

Tao Zhexuan a déclaré qu’il avait besoin de simuler grossièrement la stratégie de réécriture de Lean4 et d’apporter des modifications ciblées à de longues expressions d’une ligne à l’autre par le biais d’opérations telles que le copier-coller. Cela peut entraîner la propagation de fautes de frappe sur plusieurs lignes du document.

Lean4 peut effectuer cette réécriture de manière automatisée et vérifiable.

Bien sûr, le Lean 4 n’est pas une panacée pour le moment, et il y a quelques limites. Par exemple, il n’est pas toujours facile de réécrire des expressions impliquant des variables de contrainte.

Tao Zhexuan a déclaré qu’il attendait avec impatience le moment où il sera facile d’utiliser le langage naturel pour demander à LLM de faire une telle conversion.

Dans la fosse GPT-4 + GitHub Copilot, Crazy Amway

Dès le début du mois de septembre, Tao Zhexuan a publié un article louant l’effet de ChatGPT dans la génération de code Python - économisant directement une demi-heure de charge de travail !

À titre expérimental, il a demandé à ChatGPT d’écrire un morceau de code Python qui calcule la longueur M(n) de la plus longue sous-séquence de 1,...,n pour chaque entier naturel n, où la φ de la fonction omnipotente d’Euler ne diminue pas.

Par exemple, M(6)=5 car φ est non décroissante sur 1,2,3,4,5 (ou 1,2,3,4,6) mais pas sur 1,2,3,4,5,6.

Il est intéressant de noter qu’il a généré un morceau de code extrêmement ingénieux pour calculer des fonctions omnipotentes, qui était si ingénieux que Tao a dû le regarder pendant plusieurs minutes avant de comprendre quel était le principe derrière le code.

Bien sûr, ce code est également biaisé - il ne considère que les sous-séquences d’entiers continus, pas les sous-séquences arbitraires.

Cependant, c’est assez proche, en utilisant ce code initial généré par ChatGPT comme point de départ, Tao Zhexuan a finalement généré manuellement le code qu’il voulait, ce qui lui a permis d’économiser environ une demi-heure de travail.

Étant donné que les résultats donnés par ChatGPT sont très bons, Tao Zhexuan a déclaré qu’il l’utiliserait souvent à l’avenir pour fournir un code initial pour des calculs similaires.

Bientôt, Tao Zhexuan a de nouveau posté qu’il était entré dans GitHub Copilot sous la recommandation d’internautes !

Comme on pouvait s’y attendre, la performance subséquente de Copilot a été une véritable surprise pour lui : il suffit de donner le paragraphe d’ouverture et d’ajouter une phrase, l’IA a recommandé quelque chose de très proche de sa propre vision.

Tao Zhexuan n’a besoin que d’apporter de légères modifications à ces suggestions, et il peut les compléter en moins de la moitié du temps initialement prévu.

En octobre, Tao Zhexuan a découvert que bien que GPT-4 ne puisse pas fournir d’aide directe pour le jeu, lorsqu’il a commencé à utiliser Lean, GPT-4 est devenu très utile.

Au fur et à mesure que les niveaux deviennent de plus en plus difficiles, le rôle de GPT commence à se manifester.

Dans les cas où il est évident que Z est le résultat de X et Y, demander à GPT « Comment puis-je prouver Z si je connais déjà X et Y ? » peut résoudre toutes sortes de problèmes grammaticaux subtils dans le processus.

En plus du contenu professionnel, Tao Zhexuan a découvert qu’il pouvait utiliser DALL· E 3 et a immédiatement commencé à jouer.

Netizen : LLM peut rendre les excellentes personnes 10 000 fois meilleures

Le fait que le grand dieu soit si obsédé par les outils d’IA dans la recherche mathématique a également suscité des discussions animées parmi les internautes.

Certaines personnes ont dit qu’Okami a commencé à apprendre Lean4 avec l’aide de GPT-4 plus tôt ce mois-ci, et de temps en temps, il enregistrera ses progrès d’apprentissage sur mastodonte.

Cela montre également que pour les personnes qui réussissent le mieux, les LLM peuvent accélérer leur travail.

Certaines personnes disent que même les personnes qui ne savent pas écrire de code, tant qu’elles sont de bonnes communicantes LLM, peuvent rapidement automatiser des fonctions.

Cependant, si seules des personnes hautement qualifiées peuvent utiliser efficacement les LLM, il en résulte une augmentation des inégalités entre les personnes.

Quelqu’un s’est immédiatement manifesté pour dire que c’était vrai, son ami ne savait rien écrire d’autre que des formules Excel, mais maintenant, il peut écrire des applications Python avec GPT-4 !

En tant que codeur avec 30 ans d’expérience dans le développement, il doit également le supplier de lui enseigner cette technologie.

Son succès est probablement dû à sa capacité à communiquer avec les LLM.

Il a été prédit qu’au fil du temps, les personnes qui utilisent des LLM récolteront des avantages écrasants, quelle que soit leur propre intelligence, et qu’elles graviront de plus en plus haut l’échelle pour devenir des experts en examen.

Pour l’élite, ils peuvent obtenir un coup de pouce de 100 fois des LLM, et pour les meilleurs ingénieurs, c’est environ 10 000 fois le coup de pouce.

Ressources: