Hice por intuición una demostración de la conjetura de Conway
Un matemático aficionado describe cómo usó modelos de lenguaje grandes y el asistente de pruebas Lean para “ir por intuición” hasta una demostración formal de la conjetura de refinamiento de los números surrealistas de Conway, desatando un debate sobre autoría, crédito y qué significa “entender” un resultado. Los comentaristas profundizan en cómo se construyen los números surrealistas, el papel de la visualización y la intuición frente al formalismo, y si las pruebas impulsadas por IA sin comprensión humana avanzan o dañan la cultura matemática. El hilo se amplía hacia preguntas sobre los límites de la IA en matemáticas, el impacto en las carreras e incentivos en matemáticas puras, y si el trabajo futuro debería priorizar la comprensión conceptual sobre la resolución bruta de problemas por máquinas.
Números surrealistas y “nada vs cero”
- Muchos lectores se atascaron en el paso “entre nada y cero / entre cero y nada”.
- Varios comentaristas reexplicaron los surrealistas en términos conjuntistas: números como
{L | R}con L,R como conjuntos de surrealistas anteriores;∅|∅como 0,∅|{0}como –1,{0}|∅como 1, etc. - Las aclaraciones subrayaban: “nada” = conjunto vacío, no 0; los huecos incluyen “a la izquierda de todo” y “a la derecha de todo”.
- Se recomendaron diagramas e introducciones externas (p. ej., Hackenbush, otros blogs) por ser más claros que las definiciones en bruto.
- Las preguntas sobre cómo aparecen los irracionales y los infinitos se respondieron mediante etapas infinitas: construcciones tipo corte de Dedekind y conjuntos infinitos a izquierda/derecha generan reales, ordinales infinitos e infinitesimales.
Tutoría de IA y pedagogía
- Algunos desean tutores interactivos adaptativos, estilo RL, que modelen la comprensión individual y llenen los huecos.
- Entre las sugerencias estuvieron pedir analogías en dominios que uno ya conoce y usar configuraciones existentes de “habilidades de enseñanza”.
El papel de la IA en matemáticas: poder y límites
- Debate sobre si las pruebas impulsadas por LLM son “inteligentes” o solo fuerza bruta a gran escala.
- Algunos sostienen que explorar eficientemente enormes espacios de búsqueda ya es una marca de inteligencia; otros lo comparan con CPUs de los años 80, rápidas pero “tontas”.
- La discusión teórica referencia a Busy Beaver, el problema de la parada y Gödel: cualquier sistema computacional fijo (incluidos los LLM) no puede decidir todas las afirmaciones matemáticas verdaderas.
- Contraargumento: la mayoría de las proposiciones indecidibles o independientes son “feas e irrelevantes”; la matemática práctica rara vez choca con estos límites.
Verificación, Lean y confianza
- La formalización en Lean se considera central: si el archivo puente pequeño y el kernel son correctos, la prueba se sostiene.
- A algunos les preocupan errores en Lean/el kernel y recientes “hackeos” con LLM; otros señalan la comprobación cruzada con kernels independientes y el código confiable limitado.
- Hay interés en extraer una infraestructura reutilizable sobre números surrealistas para incorporarla a las bibliotecas principales de Lean.
Crédito, autoría y cultura matemática
- Fuerte desacuerdo sobre llamar a esto “mi prueba”:
- Un lado: usar un LLM es como usar una herramienta poderosa (un taladro); el humano eligió el problema, orquestó ejecuciones, curó resultados y asume la responsabilidad por los errores.
- El lado opuesto: el humano aportó casi ninguna intuición matemática, así que atribuirse el mérito es engañoso y corrosivo culturalmente.
- Preocupaciones más amplias:
- “Minería a cielo abierto” de la matemática para obtener resultados sin comprender puede desmotivar a los investigadores humanos y dañar las estructuras de carrera.
- Temor de que los matemáticos de nivel intermedio pierdan oportunidades ya escasas, mientras solo se beneficien unas pocas figuras senior o problemas famosos.
- Otros responden que sistematizar, simplificar y convertir pruebas oscuras de IA en demostraciones humanas cortas y elegantes es en sí mismo un trabajo sustancial.
Reacciones al proyecto y a su estilo
- Muchos lectores disfrutaron la publicación como “arte escénico epistémico” y una narrativa inusualmente accesible y autoconsciente del trabajo con modelos falibles.
- Algunos apreciaron ver a un “amateur” tropezar con matemáticas de alto nivel, encontrándolo más cercano que las charlas de expertos.
- Los escépticos encontraron el proyecto “inmoral”, poco creativo o poco útil para la comprensión, aunque reconocen que el resultado subyacente (si es correcto) es matemáticamente no trivial.
- Un experto humano clave en el área subyacente informa que el método generado por IA parece sólido y que las ideas centrales pueden destilarse en una prueba muy corta y elegante, reforzando la esperanza en una colaboración constructiva entre IA y humanos.