La IA de Anthropic alcanza el "Santo Grial" de las matemáticas

Anthropic publicó una demostración verificada por máquina de una de las conjeturas no resueltas más conocidas de la teoría de probabilidades. Un modelo de inteligencia artificial mostró que, en el problema clásico de la percolación, la transición de fase permanece continua en todas las dimensiones, cerrando el hueco para espacios de tres a diez dimensiones. La propia demostración ya está siendo verificada por un sistema de matemáticas formales; sin embargo, la revisión independiente por parte de especialistas aún no se ha completado.

La teoría de la percolación estudia cómo un conjunto de conexiones aleatorias de pronto se transforma en una red única y extensa. Es más sencillo imaginar el modelo como una malla infinita de tuberías: cada tramo está abierto de forma independiente con probabilidad p. Mientras hay pocos tramos abiertos, el agua sólo podrá circular por zonas pequeñas. Tras cierto valor crítico p_c surge la probabilidad de construir un camino que se extienda indefinidamente.

El principal enigma se refería al propio momento de la transición. Los matemáticos querían saber si ya existe una región conectada infinita exactamente en p = p_c, o si sólo aparece después de cruzar el punto crítico. En el lenguaje de la teoría de probabilidades la pregunta se expresa como θ(p_c) = 0. Un valor nulo significa que en el punto crítico aún no existe un cúmulo infinito y que la transición es continua.

El nuevo trabajo no calcula el valor de p_c. Esa formulación sería incorrecta: las probabilidades críticas exactas para la mayoría de las mallas multidimensionales siguen siendo desconocidas. El modelo de Anthropic demostró otra afirmación, no menos importante, relativa al comportamiento del sistema directamente en el umbral de la transición de fase. Para el caso bidimensional el resultado se conocía desde hace tiempo, y los métodos para espacios de alta dimensión permitían cubrir el caso de 11 dimensiones y superiores. Quedaban por cubrir las dimensiones de tres a diez, y precisamente ese vacío lo cierra ahora la nueva demostración.

La IA no intentó abordar directamente la malla infinita en toda su complejidad. La clave fue la reducción del problema publicada en 2024 a otra afirmación. Gady Kozma y Shahaf Nitzan mostraron que la famosa conjetura se sigue de cierta desigualdad para las probabilidades de conexión entre partes de un grafo aleatorio. Esa desigualdad en su momento permanecía como conjetura.

El modelo de Anthropic fue más allá y demostró una desigualdad más fuerte, de la que la afirmación necesaria de Kozma y Nitzan se obtiene como consecuencia. A partir de ahí, la cadena formal conduce a θ(p_c) = 0 para la percolación por aristas entre vecinos más cercanos en la red Z^d para cualquier dimensión d ≥ 2. La demostración publicada vuelve a derivar también una serie de resultados clásicos necesarios para toda la cadena, en vez de limitase a aceptarlos sin verificación.

La particularidad del trabajo es que los razonamientos matemáticos están escritos no sólo en texto convencional. Los autores los formalizaron en el lenguaje Lean, donde el ordenador verifica cada transición lógica. Este enfoque contrasta radicalmente con la situación en la que un modelo de lenguaje genera fórmulas que suenan convincentes y una persona debe buscar el error oculto entre decenas de páginas de razonamientos.

La verificación formal, sin embargo, no pone el punto final. Lean confirma que la deducción realmente se sigue de las definiciones y suposiciones registradas y que dentro de la demostración formal no hay pasos lógicos omitidos. Pero el ordenador no resuelve otra cuestión importante: si la afirmación formalizada coincide en todos los detalles con la conjetura matemática que se pretendía demostrar. En los materiales del proyecto se indica explícitamente que la revisión independiente aún no se ha realizado, por lo que los especialistas deberán comprobar la propia formulación y el sentido matemático de la formalización.

Hasta hace poco los modelos se probaban sobre todo con problemas de olimpiadas y teoremas ya conocidos; ahora los sistemas encuentran contraejemplos y construyen demostraciones para problemas que durante décadas ocuparon a matemáticos profesionales. No obstante, una demostración correcta no siempre equivale automáticamente a un descubrimiento científico completo: es necesario verificar la novedad del resultado, la correspondencia con el problema original, las ideas utilizadas y las posibles conexiones con trabajos anteriores.

Si la verificación independiente confirma la formalización, los matemáticos obtendrán finalmente una respuesta general para la malla clásica en cualquier dimensión: en el punto crítico no surge un cúmulo conectado infinito. No menos importante será la manera en que se obtuvo la respuesta. Aquí la IA no actuó como calculadora o buscador, sino como un sistema que construyó un nuevo argumento matemático y lo llevó a una forma que otro ordenador puede verificar línea por línea.