Par ailleurs, après des incitations supplémentaires, ChatGPT a également su adapter l'argument pour traiter à la fois de grands et de petits paramètres, aboutissant finalement à un nouveau résultat dans l'esprit de la question initiale, disponible ici https://drive.google.com/file/d/1xRw8_o2C8HwmxMDnBR5OJlxXaW7jlYbz/view?usp=sharing. De manière intéressante, la preuve contenait quelques erreurs mineures, mais l'outil d'IA Aristotle a pu corriger automatiquement ces lacunes, produisant ainsi une preuve vérifiée par Lean. À ce stade, un troisième participant a fait exécuter à Aristotle la preuve Lean existante afin d'obtenir une version plus concise. Cette version raccourcie a ensuite été transmise à un autre participant, qui l’a introduite dans une longue session de discussion avec ChatGPT https://chatgpt.com/share/695e7cbd-605c-8010-809b-ccba75560c76, dans le but de la transformer en un article beaucoup plus développé. Ce dernier ne se contentait pas de décrire la preuve, mais intégrait également ses liens avec la littérature antérieure et adoptait une structure narrative plus fluide et cohérente. Le résultat a été une nouvelle réécriture de la preuve https://drive.google.com/file/d/1MRQfcHhrYMfMTvlZcMC3zEK7aOrUyHiQ/view?usp=sharing, qui perdait de l’aspect générique typique des documents produits par une IA. À mon avis, le niveau d’écriture atteint est globalement conforme aux standards acceptables pour un article de recherche, bien qu’il reste un certain potentiel d’amélioration. Une analyse détaillée de ce texte est disponible ici https://www.erdosproblems.com/forum/thread/728#post-2852. (4/5)