Lean4 aide à repérer un petit bug dans un récent article de Terence Tao

• Publication de Terence Tao sur mathstodon.xyz
• Découverte d’un bug mineur mais important dans un récent article de Terence Tao grâce à un projet de formalisation en Lean4
• Bug repéré lors du processus de formalisation à la page 6 de l’article, consultable sur https://arxiv.org/pdf/2310.05328.pdf
• Dans l’article de Tao, l’expression divergente 12log⁡n−1n−k−1 a été trouvée pour le cas n=3, k=2
• Le problème n’existe que pour de petites valeurs de n et peut être corrigé en modifiant certaines constantes numériques de la page
• Pour n≥8, le raisonnement reste valide, et les cas de petit n peuvent être traités par une méthode plus simple
• Lean4 a demandé à Tao de prouver 0<n−3, mais il ne disposait que de l’hypothèse n>2, ce qui a fait apparaître une contradiction
• Tao prévoit d’ajouter dans une nouvelle version de l’article une note de bas de page reconnaissant cette légère erreur, découverte après sa tentative de formalisation dans Lean4
• Cette publication a suscité l’intérêt et des réactions positives de la communauté, tout en soulignant l’importance des assistants de preuve pour établir des bases solides pour les travaux futurs

[GN⁺]

Commentaires sur Hacker News

• Le mathématicien de renom Terence Tao a utilisé Lean4 et GPT4 pour repérer un petit bug dans un article récent.
• Le parcours d’apprentissage de Tao avec Lean4 a été documenté dans ses publications Mastodon, ce qui en fait une étude de cas intéressante sur la manière dont Lean4 peut accélérer le travail.
• Pour les débutants, le Natural Number Game est recommandé comme introduction facile à Lean4.
• Un utilisateur a partagé son expérience d’utilisation de TLA+ de Lamport pour produire des spécifications formelles et réduire les erreurs en programmation.
• Il existe un intérêt pour les types dépendants, malgré la complexité de leur implémentation dans les compilateurs.
• La combinaison de Lean4 et de la démonstration automatique semble être un assemblage technologique prometteur pour l’avenir, avec le potentiel de favoriser de nouvelles découvertes.
• Le fait que Tao apprenne Lean avec Copilot a été mis en avant comme un exemple de la manière dont Lean4 peut réduire les frictions liées à l’adoption de nouveaux outils.
• Les progrès de Tao avec Lean4 peuvent être consultés sur son GitHub.
• Un utilisateur a proposé l’idée de combiner un vérificateur de preuves formelles et un modèle de langage pour générer des paires synthétiques conjecture-preuve, avec un potentiel d’évolution vers des capacités surhumaines en génération de preuves.
• Le terme "bug" a été utilisé pour décrire une erreur mathématique, ce que certains utilisateurs ont trouvé inhabituel.