Las máquinas pueden ayudar a detectar errores matemáticos
Alamy Foto de stock
Un lenguaje informático creado para detectar errores en teoremas matemáticos ha descubierto por primera vez un error fundamental en un artículo de física ampliamente citado. El investigador detrás del descubrimiento dice que es el primer artículo de física que analiza de esta manera, lo que plantea una pregunta preocupante: ¿cuántos más contienen errores?
Se utiliza cada vez más software especializado para ayudar a los matemáticos a comprobar que sus pruebas son correctas y están libres de contradicciones y agujeros lógicos, mediante un proceso conocido como formalización. El enfoque incluso se ha propuesto como una solución potencial a algunos de los problemas más espinosos de las matemáticas, como la extensa prueba de 500 páginas de Shinichi Mochizuki para la conjetura ABC, sobre la cual los expertos han discutido durante años.
Ahora, Joseph Tooby-Smith de la Universidad de Bath, Reino Unido, ha volcado un lenguaje de formalización llamado Lean hacia el campo de la física. Intentó formalizar la investigación publicada en 2006 sobre la estabilidad del potencial del modelo de dos dobletes de Higgs (2HDM), que ha sido ampliamente citada en los años posteriores, pero accidentalmente reveló un error que socava el teorema.
Los teoremas formalizados se pueden utilizar como bloques de construcción para formalizar teoremas más complejos, y Tooby-Smith dice que se suponía que su trabajo sería un “ejercicio de marcar casillas” para agregar el artículo a un proyecto más amplio de investigación en física formalizada llamado PhysLib, modelado sobre una base de datos establecida para matemáticas llamada MathsLib. “No vamos a refutar artículos; vamos a salir a generar resultados que todos puedan utilizar”, dice Tooby-Smith.
El error se relaciona con una afirmación en la que los autores originales dicen que cierta condición, C, es suficiente para una solución estable del problema. Pero Tooby-Smith demostró durante la formalización que existe una condición C que no proporciona una solución estable.
Tooby-Smith dice que el descubrimiento del error tiene un efecto dramático en el artículo, pero es poco probable que cause problemas posteriores en el trabajo que se basó en él y lo citó. Sin embargo, ahora teme que muchos artículos de física contengan errores similares, pero no está seguro de cuán amplio podría ser el problema. Él cree que esto constituye un argumento sólido para que la formalización se convierta en una parte estándar de la publicación de nuevas investigaciones.
Tooby-Smith dice que los físicos tienden a no dar tantos detalles explícitos en los teoremas como los matemáticos. “Debido a que muchos físicos no están interesados en estos detalles esenciales, a veces los pasan por alto, y ahí es donde se produce un error”, dice.
Kevin Buzzard, del Imperial College de Londres, dice que la formalización está teniendo un gran impacto en las matemáticas y que no hay razón para que la física teórica, al menos, no pueda tratarse de la misma manera. “Intentamos hacer matemáticas de esta manera y resultó ser realmente interesante”, dice.
Pero el beneficio real de la formalización en matemáticas proviene ahora del gran corpus de teoremas formalizados existentes, lo que permite a los matemáticos humanos construir más fácilmente sobre ellos y también entrenar modelos de IA que pueden ayudar a formalizar nuevos teoremas más rápidamente. Entrenar esos modelos de IA para formalizar las matemáticas requirió tiempo y muchos ejemplos concretos para usar como datos de entrenamiento, que tal vez aún no estén disponibles para la física.
“Idealmente, necesitamos un millón de líneas de física, y eso podría ser un trabajo difícil de conseguir. Si las máquinas no son muy buenas en hacer física inicialmente, entonces habrá trabajo manual al principio y, con suerte, eventualmente las máquinas tomarán el control”, dice Buzzard.
Los autores del artículo de física original no respondieron a una solicitud de comentarios de New Scientist, pero Tooby-Smith dice que les informó de su descubrimiento, recibió confirmación de que estaban de acuerdo y le dijeron que se publicaría una fe de erratas.
Temas: