Hace unos meses, los resultados matemáticos de IA comenzaron a aparecer en las noticias. Naturalmente, me puse curioso sobre si yo, un novato en matemáticas, puedo encontrar un problema abierto y tener un modelo frontier resolviéndolo. Me tomó todo un mes de tiempo libre y una gran cantidad de tokens, pero creo haber obtenido una prueba de Lean de la conjetura de refinamiento de Conway, planteada hace 50 años.

La conjetura afirma que si ab = cd, existen enteros e, f, g, h tales que a = ef, b = gh, c = eg y d = fh. Mi prueba no ha sido verificada independientemente por matemáticos. Sin embargo, tengo buenas razones para creer que es correcta y realmente invito una refutación.

La prueba ha pasado por verificaciones mecánicas del registro Palomar, y las personas familiarizadas con Lean y el campo dijeron que la afirmación parece correcta. Por lo tanto, asumiendo que no dependa de un error en el núcleo, es probablemente legítima. En este post, describiré mi enfoque y las cosas aprendidas.

Elegir el campo Le pedí a Claude que elija un problema abierto en números surreales. Los números surreales son una invención de John Conway, un sistema numérico que contiene todos los números grandes y pequeños: todos los números reales, números ordinales como el infinitamente grande omega, y combinaciones como 75 + omega*3 + 1/omega. Lo maravilloso es que este rico sistema surge de una sola regla: generar un nuevo número en cada hueco entre los números que ya tienen.

Elegir el problema Inicialmente, le pedí a Claude problemas sin resolver en el programa de investigación de números surreales.