Lean4 ayuda a encontrar un pequeño bug en un artículo reciente de Terence Tao

• Publicación de Terence Tao en mathstodon.xyz
• Se descubrió un bug pequeño pero importante en un artículo reciente de Terence Tao debido a un proyecto de formalización en Lean4
• El bug fue encontrado durante el proceso de formalización en la página 6 del artículo; el artículo puede consultarse en https://arxiv.org/pdf/2310.05328.pdf
• En el artículo de Tao se encontró la expresión divergente 12log⁡n−1n−k−1 en el caso n=3, k=2
• El problema existe solo para valores pequeños de n y puede resolverse cambiando algunas constantes numéricas en la página
• Para n≥8, la lógica sigue siendo válida, y los casos de n pequeños pueden tratarse con un método más simple
• Lean4 le pidió a Tao demostrar 0<n−3, pero él solo tenía la hipótesis n>2, lo que produjo una contradicción
• Tao planea agregar una nota al pie en una nueva versión del artículo reconociendo el pequeño error detectado tras intentar la formalización en Lean4
• Esta publicación despertó interés y reacciones positivas en la comunidad, y subraya la importancia de los asistentes de prueba para establecer una base sólida para trabajos futuros

[GN⁺]

Opinión de Hacker News

• El famoso matemático Terence Tao usó Lean4 y GPT4 para encontrar un pequeño bug en un artículo reciente.
• El proceso de aprendizaje de Lean4 de Tao quedó documentado en sus publicaciones de Mastodon, convirtiéndose en un interesante caso de estudio sobre cómo Lean4 puede acelerar el trabajo.
• Para principiantes, se recomienda Natural Number Game como una introducción sencilla a Lean4.
• Un usuario compartió su experiencia usando TLA+ de Lamport para crear especificaciones formales y reducir errores en programación.
• Existe interés en los tipos dependientes, a pesar de la complejidad que implica implementarlos en compiladores.
• La combinación de Lean4 y la demostración automática parece una prometedora combinación tecnológica para el futuro, con potencial para impulsar nuevos descubrimientos.
• Se destacó que Tao aprendiera Lean usando Copilot como un ejemplo de cómo Lean4 puede reducir la fricción al adoptar nuevas herramientas.
• El progreso de Tao con Lean4 puede revisarse en su GitHub.
• Un usuario propuso la idea de combinar verificadores formales de pruebas y modelos de lenguaje para generar pares sintéticos de conjetura-demostración, lo que podría escalar hasta capacidades sobrehumanas en la generación de pruebas.
• El término "bug" se usó para describir un error matemático, algo que a algunos usuarios les pareció peculiar.