La laguna en el artículo de Tao Zhexuan fue descubierta por IA, ¡y la predicción de 26 años se hará realidad! Adivinando la dirección de la investigación mirando el nombre del teorema, el gran dios llamó asombrosa a la habilidad de la IA

Fuente del artículo: New Zhiyuan

Recientemente, Tao Zhexuan, un dios de las matemáticas que está interesado en usar GPT-4 y Copilot para investigar, descubrió un error oculto en su artículo con la ayuda de la IA.

Tao Zhexuan dijo que en el proceso de formalizar el argumento en la página 6 con Lean4, encontró que las expresiones

En n = 3 y k = 2, en realidad es divergente.

Este error no tan obvio se detectó a tiempo gracias a Lean4.

La razón es que Lean le pidió que construyera 02. Como resultado, Lean no puede basarse en un 0 negativo

Afortunadamente, este es solo un error menor que solo existe cuando el valor n es pequeño. En este punto, solo necesita modificar algunas constantes en el papel.

Algunos fanáticos entusiastas de las matemáticas exclamaron en esta publicación: Esto es increíble, y es genial ver la propagación de los asistentes de prueba de IA, sentando una base más sólida para el futuro de la investigación matemática.

Tao Zhexuan dijo que esto es completamente posible.

Tal vez en un futuro cercano, podamos construir una capa de IA sobre Lean.
Al describir los pasos de la prueba a la IA, la IA puede usar Lean para ejecutar la prueba y, en el proceso, también puede llamar a varios paquetes de álgebra computacional.

En junio de este año, Tao Zhexuan predijo en un blog sobre la experiencia de prueba de GPT-4:

En 2026, la IA se combinará con herramientas de búsqueda y matemáticas simbólicas para convertirse en un coautor de confianza en la investigación matemática.

Durante este periodo, hay personas que siguen demostrándolo. Por ejemplo, académicos de Caltech, NVIDIA, MIT y otras instituciones han construido un demostrador de teoremas basado en LLM de código abierto.

Y Tao Zhexuan también lo practicó, y el nuevo artículo comenzó a escribirse en GPT-4, y exclamó repetidamente: ¡la increíble capacidad de GitHub Copilot me hace sentir incómodo!

AI Bendice a Dios Investigación Matemática

Recientemente, Tao Zhexuan ha "entrado por completo en el pozo" de la IA.

Con la ayuda de GPT-4, comenzó a aprender a escribir artículos e investigar matemáticas con Lean4.

Estaba tan entusiasmado con el proceso que publicaba en Mastodon cada pocas horas para registrar sus aprendizajes y experiencias.

Al escribir un artículo sobre la desigualdad de McLaughlin, Tao hizo un uso extensivo de herramientas de IA como GPT-4, Copilot y Lean4.

Dirección:

A medida que avanzamos, Tao ha completado la reparación del argumento en la Sección 2 del artículo en Lean4.

Sin embargo, el proceso fue mucho más tedioso de lo que esperaba, y cada línea de prueba tardó aproximadamente una hora en formalizarse.

Durante la primera semana del proyecto, su cuello de botella fue su falta de familiaridad con la sintaxis y las herramientas de Lean; Pero el cuello de botella actual radica en las propias herramientas, que no son tan avanzadas como las de los paquetes de álgebra computacional.

Por ejemplo, en una línea de su artículo, afirma que la desigualdad:

Se puede reorganizar como:

Suponiendo que todos los denominadores sean positivos, esta es una tarea muy rápida para los cálculos manuales y se puede hacer con bastante facilidad en cualquier paquete de álgebra computacional estándar.

Lean tiene herramientas automáticas muy útiles para manejar operaciones lineales, pero actualmente no existe ninguna herramienta para simplificar automáticamente expresiones complejas que involucren exponentes.

Por lo tanto, tenemos que lidiar con la ley exponencial y otras operaciones mencionadas anteriormente paso a paso, y este proceso lleva mucho tiempo.

Al final, Tao decidió no usar la notación asintótica en esta parte del argumento, sino establecer una desigualdad con una constante definida C:

A partir de ahí

Inicialmente, Tao pensó que sería "más sencillo" demostrar las desigualdades con valores como C=7. Sin embargo, era engorroso utilizar las herramientas existentes para probar rigurosamente C≤7, por lo que la idea se abandonó en favor de un valor C más formalmente operativo. Ahora seleccionado, el valor es de aproximadamente 6,16.

En este sentido, algunos internautas curiosos preguntaron: "¿Cómo le va a la IA para demostrar la velocidad en comparación con la aritmética manual?"

Tao Zhexuan dijo que, según sus propias observaciones, los tipos de tareas que son mecánicas para los paquetes de álgebra computacional y las calculadoras no son necesariamente mecánicas para los asistentes de pruebas formales.

Pero con la llegada de los LLM, deberíamos ser capaces de unificar todas las herramientas asistidas por ordenador en una herramienta universal y fácil de usar. Y esta herramienta tendrá todos los beneficios de cada componente.

Incluso, en un futuro próximo, también podemos imaginar la construcción de una capa de IA sobre Lean.

Los pasos de la demostración se describen a la IA en "Inglés matemático", y la IA puede intentar ejecutarlo utilizando Lean, tal vez invocando un paquete de álgebra informática en el proceso.

El copiloto puede adivinar los siguientes pasos

Anteriormente, en este artículo sobre la investigación de la desigualdad de McLaughlin, Tao Zhexuan se sorprendió al descubrir que Copilot era capaz de predecir lo que quería hacer a continuación.

No solo puede predecir correctamente las múltiples líneas de código utilizadas para varias verificaciones de rutina, sino que también puede deducir en qué dirección quiere hacer su investigación basándose en el nombre del teorema proporcionado por Tao Zhexuan.

Esto hizo que Tao Zhexuan exclamara una y otra vez: ¡Es increíble!

En el proceso de demostración del teorema 1.3 en el artículo, Tao Zhexuan usó Lean4 para completar la formalización de la demostración del teorema.

En el artículo, solo hay una página en el proceso de prueba, pero la prueba formal utiliza 200 líneas de Lean4.

Por ejemplo, en el documento, Tao Zhexuan solo asume

es convexa en cualquier número real de a>0 y la desigualdad de Jensen se llama después. Pero el código ocupa unas 50 líneas.

En el proceso, GitHub Copilot mostró todo tipo de predicciones divinas y predijo mágicamente la próxima dirección de la investigación de Tao Zhexuan.

La estrategia de reescritura de Lean le permite revisar suposiciones u objetivos extensos a través de sustituciones específicas.

Esta característica es extremadamente importante porque permite a las personas manipular libremente estas expresiones sin tener que ingresarlas en su totalidad todo el tiempo.

Comparativamente hablando, en LaTex, esta operación es mucho más engorrosa.

Tao Zhexuan dijo que necesitaba simular aproximadamente la estrategia de reescritura de Lean4 y realizar ediciones específicas en expresiones largas de una línea a la siguiente a través de operaciones como cortar y pegar. Esto puede hacer que los errores tipográficos se extiendan a lo largo de varias líneas del documento.

Lean4 puede hacer esta reescritura de forma automatizada y verificable.

Por supuesto, Lean 4 no es una panacea en este momento, y existen algunas limitaciones. Por ejemplo, reescribir expresiones que involucran variables de restricción no siempre es fácil.

Tao Zhexuan dijo que espera con ansias el momento en que sea fácil usar el lenguaje natural para pedirle a LLM que haga tal conversión.

En el foso GPT-4 + Copiloto de GitHub, Crazy Amway

Ya a principios de septiembre, Tao Zhexuan publicó un post en el que elogiaba el efecto de ChatGPT en la generación de código Python, ¡ahorrando directamente media hora de carga de trabajo!

Como experimento, le pidió a ChatGPT que escribiera un fragmento de código Python que calculara la longitud M(n) de la subsecuencia más larga de 1,...,n para cada número natural n, donde el φ de la función omnipotente de Euler no disminuye.

Por ejemplo, M(6)=5 porque φ no es decreciente en 1,2,3,4,5 (o 1,2,3,4,6) pero no en 1,2,3,4,5,6.

Curiosamente, generó un fragmento de código extremadamente ingenioso para calcular funciones omnipotentes, que era tan ingenioso que Tao tuvo que mirarlo fijamente durante varios minutos antes de entender cuál era el principio detrás del código.

Por supuesto, este código también está sesgado: solo considera subsecuencias de enteros continuos, no subsecuencias arbitrarias.

Sin embargo, esto está lo suficientemente cerca, utilizando este código inicial generado por ChatGPT como punto de partida, Tao Zhexuan finalmente generó manualmente el código que quería, lo que le ahorró alrededor de media hora de trabajo.

Dado que los resultados dados por ChatGPT son muy buenos, Tao Zhexuan dijo que lo usará a menudo en el futuro para proporcionar código inicial para cálculos similares.

¡Pronto, Tao Zhexuan volvió a publicar que había ingresado a GitHub Copilot por recomendación de los internautas!

Como era de esperar, la actuación posterior de Copilot fue una verdadera sorpresa para él: con solo dar el párrafo inicial y agregar una oración, la IA recomendó algo muy cercano a su propia visión.

Tao Zhexuan solo necesita hacer ligeras modificaciones a estas sugerencias, y puede completarlas en menos de la mitad del tiempo planeado originalmente.

En octubre, Tao Zhexuan descubrió que, aunque GPT-4 no podía proporcionar ayuda directa para el juego, cuando comenzó a usar Lean, GPT-4 se volvió muy útil.

A medida que los niveles se vuelven cada vez más difíciles, el papel de GPT comienza a mostrarse.

En los casos en los que es obvio que Z es el resultado de X e Y, preguntar a GPT "¿Cómo puedo probar Z si ya conozco X e Y?" puede resolver todo tipo de problemas gramaticales sutiles en el proceso.

Además del contenido relacionado con los profesionales, Tao Zhexuan descubrió que podía usar DALL· E 3 e inmediatamente comenzó a jugar.

Internauta: LLM puede hacer que las personas excelentes sean 10,000 veces mejores

El hecho de que el gran dios esté tan obsesionado con las herramientas de IA en la investigación matemática también ha despertado acaloradas discusiones entre los internautas.

Algunas personas dijeron que Okami comenzó a aprender Lean4 con la ayuda de GPT-4 a principios de este mes, y de vez en cuando registrará su progreso de aprendizaje en mastodon.

También muestra que para las personas más exitosas, los LLM pueden acelerar su trabajo.

Algunas personas dicen que incluso las personas que no pueden escribir código, siempre y cuando sean un buen comunicador LLM, pueden automatizar funciones rápidamente.

Sin embargo, si solo las personas altamente calificadas pueden usar los LLM de manera efectiva, el resultado es que la desigualdad entre las personas puede aumentar.

Alguien inmediatamente se adelantó para decir que era cierto, su amigo no podía escribir nada excepto fórmulas de Excel, pero ahora, ¡puede escribir aplicaciones de Python con GPT-4!

Como programador con 30 años de experiencia en desarrollo, también necesita rogarle que le enseñe esta tecnología.

Su éxito se debe probablemente a su capacidad para comunicarse con los LLM.

Se ha predicho que, con el tiempo, las personas que utilizan los LLM obtendrán beneficios abrumadores, independientemente de su propia inteligencia, y ascenderán cada vez más en la escalera para convertirse en expertos en exámenes.

Para la élite, pueden obtener un aumento de 100 veces de los LLM, y para los mejores ingenieros, es aproximadamente 10,000 veces el impulso.

Recursos: