A Terence Tao le gusta! ChatGPT demuestra automáticamente un gran avance, y la IA dominará el mundo de las matemáticas en 10 años

**Fuente:**Xinzhiyuan

**Guía:**Aunque muchas personas no quieren admitirlo, es muy probable que la IA supere a los matemáticos humanos dentro de diez años.

Hace unos días, un artículo de Caltech e investigadores del MIT que usaban ChatGPT para probar teoremas matemáticos explotó y atrajo gran atención en el círculo matemático.

Jim Fan, el científico jefe de Nvidia, lo reenvió con entusiasmo, diciendo que el Copiloto de matemáticas de IA ha llegado, ¡y la próxima persona que descubra nuevos teoremas será un matemático de IA completamente automático!

The New York Times también publicó un artículo recientemente, diciendo que los matemáticos están listos y que la IA alcanzará o incluso superará a los mejores matemáticos humanos dentro de diez años.

Y el propio Tao Zhexuan volvió a publicar este artículo.

Siobhan Roberts participó en el taller IPAM de este año realizado por Machine Assisted Proofs, y luego escribió este artículo sobre IA y matemáticas basado en su propia experiencia y entrevistas.

**¡La IA también viene a subvertir el mundo de las matemáticas! **

Hoy, los matemáticos tienen que enfrentarse a la última fuerza revolucionaria: la IA.

En 2019, el científico informático Christian Szegedy, ex empleado de Google que ahora trabaja en una startup del Área de la Bahía, predijo que los sistemas informáticos igualarían o superarían las habilidades de resolución de problemas de los mejores matemáticos humanos en una década. El año pasado, revisó la fecha objetivo a 2026.

Jeremy Avigad, lógico de la Universidad Carnegie Mellon (en azul) con estudiantes en la Escuela de Verano de Matemáticas Formales

Akshay Venkatesh, ganador de la Medalla Fields de 2018 y matemático del Instituto de Estudios Avanzados de Princeton, actualmente no está interesado en usar IA, pero está muy interesado en discutir temas relacionados con la IA.

En una entrevista el año pasado, Venkatesh dijo: "Quiero que mis alumnos se den cuenta de que este campo va a cambiar mucho".

Y recientemente su actitud es: "No tengo ninguna objeción al uso deliberado, incluso deliberado, de la IA para ayudar a la comprensión humana. Pero creo firmemente que debemos ser conscientes y cautelosos sobre la forma en que la usamos".

En febrero de este año, el Instituto de Matemáticas Teóricas y Aplicadas de la UCLA realizó un taller sobre "Pruebas asistidas por máquinas".

El principal organizador del seminario es Tao Terence, un matemático que ganó la Medalla Fields en 2006 y trabaja en UCLA.

Señaló que el uso de la IA para ayudar en las pruebas matemáticas es en realidad un fenómeno digno de atención.

Solo en los últimos años los matemáticos han comenzado a preocuparse por la amenaza potencial de la IA, ya sea la destrucción de la estética matemática por parte de la IA o la amenaza para los propios matemáticos.

Y miembros destacados de la comunidad están poniendo estos temas sobre la mesa y comenzando a explorar cómo "romper el tabú".

Los organizadores de la escuela de verano, de izquierda a derecha: Avigad, Patrick Massot y Heather Macbeth

De las primitivas de la geometría euclidiana al código informático

Durante milenios, los matemáticos se han adaptado a los últimos avances en lógica y razonamiento. Pero, ¿están listos para la IA?

Retrato del matemático griego Euclides del siglo XVII en el Museo Getty de Los Ángeles: está vestido con harapos y sostiene su tratado de geometría, Elementos

Durante más de 2000 años, el texto de Euclides ha sido el paradigma de la argumentación y el razonamiento matemático.

Jeremy Avigad, lógico de la Universidad Carnegie Mellon, dice que Euclides comenzó con una "definición" casi poética sobre la cual construir las matemáticas de su tiempo, usando conceptos básicos, definiciones y teoremas previos, cada uno de ellos sucesivo. Todos los pasos "siguen claramente" a los pasos anteriores, en manera de probar las cosas.

Algunos se quejaron de que algunos de los pasos "obvios" de Euclid no eran tan obvios, pero el Dr. Avigad dijo que el sistema funcionó.

Pero después del siglo XX, los matemáticos ya no estaban dispuestos a basar las matemáticas en esta base geométrica intuitiva.

En cambio, desarrollaron sistemas formales con representaciones simbólicas precisas y reglas mecánicas.

Eventualmente, bajo tal sistema, las matemáticas podrían traducirse a código de computadora.

En 1976, el teorema de los cuatro colores se convirtió en el primer teorema importante que se demostró con la ayuda de cálculos de fuerza bruta.

El teorema de los cuatro colores: cuatro colores son suficientes para llenar un mapa de modo que no haya dos regiones adyacentes que tengan el mismo color

IA que se queja: Lo siento, no puedo entender tu teorema

Existe un dispositivo matemático de este tipo llamado Proof Assistant o Interactive Theorem Prover.

Paso a paso, los matemáticos convierten las demostraciones en código y luego usan programas de software para comprobar que el razonamiento es correcto.

El proceso de verificación se acumula en una biblioteca de referencia de especificación dinámica, que está disponible para otros.

El Dr. Avigad, director del Centro Hoskinson de Matemáticas Formales, dijo que este tipo de formalización sentó las bases de las matemáticas de hoy, al igual que Euclides trató de transcodificar las matemáticas de esa época, brindándoles así una base.

Recientemente, Lean, un sistema asistente de pruebas de código abierto, ha vuelto a atraer mucha atención.

Lean fue desarrollado por el actual científico informático de Amazon, Leonardo de Moura, mientras trabajaba en Microsoft.

Lean utiliza un razonamiento automatizado, impulsado por la IA GOFAI de la vieja escuela, una IA simbólica inspirada en la lógica.

Hasta ahora, Lean ha verificado un teorema interesante que convierte una esfera de adentro hacia afuera, así como un teorema clave que unifica esquemas en toda la esfera matemática.

Sin embargo, el asistente de prueba también tiene deficiencias: a menudo se quejará de que no comprende las definiciones, los axiomas o los pasos de razonamiento introducidos por el matemático, por lo que también se le llama "queja de prueba".

Esas quejas harían que la investigación fuera engorrosa, pero el tipo de funcionalidad que proporciona retroalimentación línea por línea también haría que el sistema fuera útil para la enseñanza, dice Heather Macbeth, matemática de la Universidad de Fordham.

Esta primavera, la Dra. Macbeth diseñó un curso "bilingüe". Tradujo todos los problemas de la pizarra al código Lean en las notas de clase, y los estudiantes deben presentar soluciones en Lean y lenguaje natural.

"Les dio confianza", dijo el Dr. Macbeth, porque recibirían información instantánea sobre cuándo se completó la prueba y si cada paso del camino fue correcto o incorrecto.

Y después de asistir a un taller, la matemática Emily Riehl de la Universidad Johns Hopkins lo intentó.

Emily Riehl, matemática de la Universidad Johns Hopkins, ha estado usando un asistente de prueba experimental

Usó un subprograma asistente de prueba para probar los teoremas en sus artículos publicados anteriormente.

Después de usarlo, se sorprendió. "Ahora entiendo el proceso de prueba mucho más profundamente que nunca. Mi pensamiento es tan claro que puedo explicárselo a la computadora más tonta".

Un proyecto grupal en el que participaron los estudiantes durante la Escuela de Verano de Formalización Matemática

**Razonamiento violento: esto no es "matemático" **

Otra herramienta que los informáticos suelen utilizar para resolver algunos problemas matemáticos se llama "razonamiento violento", pero la comunidad matemática a menudo se burla de este método.

Sin embargo, a los científicos de IA no parece importarles mucho las ideas de los matemáticos y continúan usando sus propios métodos familiares para capturar las "tierras altas" de las matemáticas.

Heule, un científico informático de la Universidad Carnegie Mellon, utilizó un archivo "SAT solver" de 200T para resolver el "problema triple booleano de Pitágoras" en 2016.

La revista "Nature" dijo en el artículo: La prueba de 200T es el proceso de prueba más grande de la historia. ¿Es realmente matemática usar estas herramientas para resolver problemas?

Pero en opinión del científico informático Heule, el autor del artículo sobre cómo resolver el problema, "este enfoque es necesario para resolver problemas más allá del alcance de las capacidades humanas".

De manera similar, después de derrotar a humanos en un juego de ajedrez (AlphaZero), DeepMind diseñó algoritmos de aprendizaje automático para resolver el plegamiento de proteínas (AlphaFold).

DeepMind publicó un artículo argumentando que la forma en que lograron estos resultados fue mediante el uso de IA para guiar la intuición humana para avanzar en las matemáticas.

Yuhuai Wu, un ex científico informático de Google que ahora está iniciando un negocio en el Área de la Bahía, también dijo que la dirección de su negocio es utilizar el aprendizaje automático para resolver problemas matemáticos.

Su proyecto actual, Minerva, es un modelo de lenguaje grande perfeccionado para resolver modelos matemáticos.

En el futuro, espera que el proyecto se convierta en un "matemático automatizado" que pueda "resolver problemas matemáticos de forma independiente" como asistente general de investigación.

Las matemáticas son una prueba de fuego

Por otro lado, muchos matemáticos que han estado en contacto profundo con la tecnología de IA también expresaron su preocupación de que la IA no se toma en serio en la investigación matemática.

Creen que la tecnología de inteligencia artificial a menudo puede ayudar "directamente" a los matemáticos a "encontrar" las respuestas que buscan.

Aunque los matemáticos o los expertos en IA no tienen idea de cómo la IA encontró esta respuesta.

Geordie Williamson, un matemático que ha trabajado con DeepMind, compartió una vez una experiencia de trabajo con DeepMind.

En el proceso de su cooperación con DeepMind, una red neuronal descubierta por DeepMind puede predecir el valor de los datos que él cree que es muy importante y es extremadamente preciso.

Se está esforzando mucho por comprender cómo lo hace la IA, porque esa podría ser la base de un teorema.

Pero al final todavía no podía entender la lógica de la IA, y la gente de DeepMind tampoco podía hacerlo.

Al igual que Euclides, las redes neuronales de alguna manera encuentran la verdad, pero las razones lógicas son difíciles de comprender.

La inferencia, por otro lado, desde el punto de vista del matemático, es la esencia de las matemáticas, pero una pieza faltante del rompecabezas en el aprendizaje automático.

En el mundo de la tecnología, el mundo de la tecnología estaría perfectamente contento si hubiera una caja negra que brindara una solución a un problema la mayor parte del tiempo.

La IA es una caja negra.

Pero los matemáticos no están satisfechos con esta situación.

Según el matemático, tratar de entender cómo funcionan las redes neuronales plantea preguntas matemáticas fascinantes.

Y resolver estos problemas permitirá a los matemáticos "hacer contribuciones significativas al mundo".

Si la IA puede demostrar teoremas matemáticos

¿Qué haríamos si el mundo se inundara de hipótesis generadas por IA?

Los internautas enviaron tortura del alma a esto, y tengo dudas sobre la nueva hipótesis/fórmula del sistema de IA como primer paso, porque DeepMind ya lo hizo en la teoría de nudos.

Me pregunto cómo responderá la comunidad a la avalancha de nuevas suposiciones que genera la IA. Una cosa es verificar un argumento lógico creado por una IA; otra es sentirse abrumado por millones de sugerencias de "oh, esto podría ser cierto". No creo que nuestros sistemas de revisión y publicación existentes estén preparados para esto.

¿Cómo afecta esto a la confianza de la gente en las matemáticas?

Se ha argumentado que las máquinas no podrán hacer matemáticas en el corto plazo, pero podría verse cambiando la forma en que se realiza la investigación de la misma manera que los modelos de aprendizaje automático y el poder computacional han cambiado el campo de la biología.

Algunos internautas dijeron que desde AlphaDev, he estado pensando en este problema, pero el mismo programa puede construir algoritmos de clasificación y también puede usar verificadores de prueba automáticos para probar teoremas matemáticos. La verdadera pregunta es si se puede usar para probar algo importante, no solo un descubrimiento trivial.

Sin embargo, algunos internautas aún se muestran escépticos acerca de si las herramientas similares a GPT realmente pueden descubrir verdades valiosas.

Algunos internautas también señalaron que puede haber una diferencia entre los humanos y la IA en la comprensión y el prestar atención a las matemáticas. La IA prueba lo que es verdad, mientras que los humanos siempre se enfocan en por qué es verdad.

Referencias: