En el sitio web de problemas de Erdős, el apoyo de IA se está volviendo cotidiano

• Durante el proceso de resolución del problema de Erdős #367, las herramientas de IA desempeñaron un papel clave, y se reportó un caso de colaboración con matemáticos humanos
• Wouter van Doorn presentó un contraejemplo generado por un humano para la segunda parte del problema, y luego Gemini Deepthink generó una prueba completa de la congruencia relacionada
• Terence Tao publicó una versión más simple de la prueba basada en teoría algebraica de números p-ádicos de Gemini, y después mencionó la posibilidad de formalizarla en Lean
• Boris Alexeev completó la formalización en Lean usando la herramienta Aristotle de Harmonic, y verificó manualmente la proposición final para evitar el mal uso de la IA
• Esta secuencia de hechos muestra que la asistencia de IA en la investigación matemática se está convirtiendo gradualmente en un procedimiento estándar

---

Un caso de colaboración con IA en el problema de Erdős #367

• El 20 de noviembre, Wouter van Doorn presentó un contraejemplo para la segunda parte del problema, que dependía de la suposición de que cierta congruencia era verdadera
  • Pidió a otros participantes que verificaran la validez de esa congruencia
• Unas horas después, Terence Tao le planteó el problema a Gemini Deepthink y, en unos 10 minutos, obtuvo una prueba completa de la congruencia y la verificación de todo el argumento
  • La prueba de Gemini usó teoría algebraica de números p-ádicos, y Tao la transformó en una prueba elemental más simple para publicarla en el sitio
  • Tao mencionó que esta prueba podría permitir una “vibe formalizing” en Lean

Formalización y verificación en Lean

• Dos días después, Boris Alexeev completó la formalización en Lean usando la herramienta Aristotle de Harmonic
  • Para evitar el uso indebido de la IA, la proposición final se formalizó manualmente de forma directa
  • Todo el proceso tomó unas 2 a 3 horas, y el resultado se publicó en línea
• Después, Tao realizó una búsqueda bibliográfica con ayuda de IA, pero aunque encontró algunos estudios relacionados, no halló nada directamente vinculado con el problema #367

Reacción y debate en la comunidad

• Algunos usuarios están siguiendo con interés, a través de las actualizaciones de Tao, el estado actual del uso académico de la IA en matemáticas
• Otros usuarios expresaron una postura crítica hacia el enfoque formalista de Lean, señalando que la comprensión matemática es compresión, mientras que Lean la descompone en detalles de bajo nivel
  • El documento relacionado “Against Lean: Why Proof Assistants Formalize the Wrong Thing” sostiene que Lean y asistentes de prueba similares capturan mal la esencia de las matemáticas
• Otro usuario mencionó los problemas de precisión en las conversaciones con IA, y evaluó que requiere ajustes finos, pero es agradable de usar

[GN⁺]

Comentarios de Hacker News

• Es sorprendente poder pasarle papers de ML centrados en matemáticas a un asistente de IA y recibir una explicación sencilla o pseudocódigo
  Para alguien como yo, que no había usado en más de 25 años lo que aprendí en la universidad, ha sido de muchísima ayuda

  • Me pregunto cómo verifican que esa explicación sea correcta. Las definiciones matemáticas tienen muchas sutilezas
  • Creo que justo aquí es donde los LLM brillan para aprender
    Puedes meter un paper en Claude, recibir un resumen y luego seguir haciendo preguntas
    Incluso en campos como la biología, que yo no estudié en la licenciatura o maestría, pude profundizar como si hablara con un tutor con conocimiento
  • La notación matemática es muy dependiente del contexto, así que si le pides a un LLM que la convierta a un lenguaje de bajo contexto como Lisp, puedes captar la estructura mucho más rápido

• Espero que investigadores y empresas obtengan más mejoras de productividad en la investigación científica
  Incluso un asistente imperfecto da suficiente apalancamiento

  • Existe una beta para iOS de la app de formalización que mencionó Tao → Aristotle
    Al parecer es una startup fundada por el CEO de Robin Hood

• El 'vibe formalizing' se siente como una extensión lógica de 'vibe engineering' y 'vibe coding'
  Cuando las piezas del problema no encajan bien, resulta interesante un enfoque tipo 'Move 37 as a Service' que combine métodos informales con rigor matemático

  • Antes me había atorado leyendo un paper sobre polyhedral compilation, y ChatGPT me guió bien en el proceso de reasoning
    Claro, también hubo partes incorrectas, pero al conversar reflejando mi propia confusión, pude profundizar mi entendimiento
    La IA es especialmente buena para detectar los puntos de confusión del usuario

• Escuché una conversación sobre cómo se pronuncia el nombre del matemático húngaro Erdős
  En húngaro, la ortografía y la pronunciación casi siempre coinciden, pero en los nombres hay excepciones
  En inglés, suena más o menos como “airdish”

  • Ő es simplemente un sonido œ (oe). La -y en nombres húngaros es un vestigio de la terminación -i que solía indicar linaje noble
    Ejemplos: Görgey, Széchényi, Lánczos
    El orden de los nombres húngaros, como en japonés, es apellido-nombre (big endian). Por ejemplo: “Erdős Pál”, “Neumann János”
  • Había un poema chistoso que vi en el tablero del departamento de matemáticas en 1960: el chiste era que un paper de Erdos refutaba el teorema de que ‘los círculos son redondos’
  • Como los signos diacríticos (marcas de pronunciación) significan cosas distintas en cada idioma, me parece raro usar marcas húngaras tal cual dentro de una oración en inglés
  • Al principio la pronunciación “airdish” me parecía rara, pero al palatalizar la terminación 'os', empezó a sonar plausible
  • Como no soy estadounidense, parece que a nadie le importan estos temas de pronunciación

• Me parece interesante que entre los comentarios haya reacciones con sesgo anti-Lean

  • No soy matemático, pero me pregunto si ese material anti-Lean es confiable
    Quisiera saber si simplemente promueve otro enfoque o si filosóficamente se opone a Lean
  • Una figura famosa como Tao inevitablemente atrae la atención de excéntricos y conspiranoicos

• Los resultados de usar IA en investigación matemática han sido mixtos
  A veces completa argumentos no triviales de manera automática, pero en algunas áreas se pierde por completo
  Por ahora, creo que la IA sigue siendo útil solo como herramienta de apoyo, más que como reemplazo de los matemáticos

  • He tenido experiencias parecidas. En un paper le pedí resolver un simple problema de cálculo de permutaciones, y terminó tomando más tiempo que hacerlo yo mismo
    En programación también hubo casos donde no detectó bugs menores, aunque en tareas complejas sí me ayudó bastante
    Al final, estas herramientas todavía están lejos de reemplazar a un experto, y venderlas de más puede terminar dañando la confianza
    Como dice la frase, si prometiste la luna, tienes que entregar la luna; es importante tener expectativas realistas

• No puedo creer que en mi vida haya llegado la era tipo Star Trek en la que puedas decir: “Computadora, dibuja la prueba de este problema matemático”
  Ojalá también fuera posible “Beam me up Scotty”

  • Aunque si murieras cada vez que pasa, entonces sí sería un problema

• Esta noche, mientras manejaba, estuve conversando con ChatGPT sobre la estructura detallada de los pipeline schedulers de LLVM y GCC
  Eso mejoró mucho mi productividad y hasta me organizó automáticamente notas sobre compiladores con los que estoy experimentando
  Antes eso era inimaginable

  • Por mi experiencia, es muy probable que el LLM se haya equivocado en parte de los detalles
    Claro, los resultados pueden variar de persona a persona

• Si le pones Erdos de nombre a una IA, parece que el Erdos number de todos sería 1

  • O daría la impresión de ser una secuela de DR-DOS
  • De hecho, existe un producto llamado Erdos, una IDE con integración de IA

• Impresiona cómo aprovechó bien las herramientas frontier existentes para construir un entorno colaborativo de investigación matemática

  • Por suerte, las matemáticas son un campo donde la idolatría o los concursos de popularidad no determinan si un resultado es verdadero o falso
    Por eso sigo pensando que las matemáticas son una de las pocas disciplinas que aún siguen libres de la influencia pseudocientífica