Resolviendo 20 problemas de Erdős con 20 cuentas de Codex ejecutándose en paralelo

Artículo original ↗ Discusión en Hacker News ↗

Los agentes de IA integrados con Lean 4 y cómputo en la nube a gran escala están generando pruebas verificadas por máquina para docenas de problemas difíciles de Erdős, lo que despierta tanto entusiasmo como inquietud sobre lo que esto significa para la investigación matemática. Los comentaristas examinan la configuración técnica, la financiación y los planes de apertura del sistema, y señalan que, aunque las pruebas formales son convincentes, convertirlas en argumentos legibles e interesantes para humanos sigue siendo un desafío aparte. El intercambio se amplía a cuestiones sobre el valor de las matemáticas puras “inútiles”, el futuro papel de los matemáticos humanos a medida que la búsqueda de pruebas se automatiza y cómo la demostración de teoremas impulsada por IA podría acabar conectándose con el impacto en el mundo real y el cambio económico.

Infraestructura, Cómputo y Acceso al Modelo

  • El proyecto usa muchas cuentas de Codex mediante tokens OAuth y un broker personalizado que distribuye el balanceo de las llamadas a la API; “ejecutar GPT localmente” fue un problema de formulación, no autoalojar el modelo.
  • El cómputo local es un servidor con múltiples vCPU; los comentaristas señalan que ese hardware es asequible para aficionados.
  • Los agentes de IA tienen herramientas bash y acceso a paquetes matemáticos preinstalados en las VM.
  • Modelos mencionados: GPT‑5.6 (para generación), Fable (para verificación/resúmenes de pruebas en Lean), Gemini embeddings.

Armazón, Código Abierto y Contribuciones

  • Las preguntas se centran en el “agentic harness”: cómo se orquestan los bucles, qué modelos “dirigen” y cómo se mide el progreso; los detalles siguen siendo de alto nivel.
  • Otro participante describe un sistema independiente similar: inferencia soberana en la intranet, trabajadores aislados para Lean/Sage, modelos de pesos abiertos y planes para un ajuste fino adicional.
  • Hay interés en publicar el sistema como código abierto y permitir contribuciones; el autor dice que el proyecto comenzó como un experimento rápido y autocontenido y quizá se abra más adelante.

Validez, Rigor y Redacción

  • Las pruebas en Lean 4 son verificadas por máquina; Fable actúa como una especie de árbitro.
  • Crítica: los resúmenes de las pruebas son técnicamente densos y están mal adaptados a lectores humanos; transformar pruebas formales en explicaciones claras y estéticas es un paso distinto, todavía ausente.
  • El autor lo reconoce y planea mejorar las redacciones.
  • Algunas soluciones de Erdős presentadas se retiraron temporalmente no por ser incorrectas, sino por un encuadre confuso o por ser solo parciales; el trabajo continúa.
  • Se sugiere integrar la herramienta “comparator” de Lean para protegerse de una sutil falta de solidez al modificar contextos.

Valor de las Matemáticas Puras y la Demostración de Teoremas con IA

  • Debate sobre si las matemáticas puras “inútiles” son autosuficientes y socialmente irrelevantes frente a su historia de aplicaciones inesperadas (p. ej., criptografía) y su valor estético intrínseco.
  • Algunos ven resolver problemas de Erdős como una referencia y una fuente de técnicas más que como una aplicación directa; el impacto en el mundo real podría venir más de problemas frontera o del Millenium.
  • Otros sostienen que, aunque sea puramente recreativo, esto es tan legítimo como cualquier afición intelectual.

Impacto en los Matemáticos y en la Sociedad

  • Hay preocupación de que los sistemas de prueba con IA puedan “quitarle la diversión a las matemáticas” y amenazar los empleos de los matemáticos; la réplica lo compara con miedos previos a la automatización (p. ej., telares, calculadoras).
  • Varios argumentan que los matemáticos pasarán a entender, conjeturar y verificar pruebas generadas por IA; las pruebas avanzadas ya suelen estar más allá de la capacidad de una sola persona.
  • Hilo más amplio sobre desacoplar el sustento del trabajo, la posible RBU y gravar a las empresas de IA; hay desacuerdo sobre cuán urgentes son los cambios de política.

Estado y Futuro de la IA en Matemáticas

  • Muchos expresan asombro de que los LLM ahora puedan resolver problemas de Erdős no triviales; la percepción está pasando de “¿pueden los LLM hacer matemáticas?” a “¿hasta dónde podemos empujar esto?”
  • Futuro esperado: autoformalización masiva de las matemáticas existentes, generación y evaluación automática de conjeturas a gran escala y, posiblemente, esfuerzos distribuidos al estilo BOINC para la exploración matemática.