Lo Que Claude Hizo Realmente
Anthropic afirmó el 4 de septiembre que Claude produjo la primera demostración completa y verificada por ordenador del último teorema de Fermat, trabajando con el asistente de demostración Lean 4 durante 11 días con solo orientación general de un investigador humano. El sistema generó 13 millones de líneas de código en Lean y demostró más de 30.000 teoremas auxiliares, de los cuales 29.500 llegaron a la demostración final verificada, usando un modelo de investigación interno que consumió unos seis mil millones de tokens de salida entre decenas de agentes que corrían en paralelo sobre la plataforma Prove2Me.
Las matemáticas de fondo no son nuevas. Andrew Wiles demostró el último teorema de Fermat en 1995, y Claude formalizó una simplificación posterior de esa demostración hecha por Darmon, Diamond y Taylor, convirtiendo un argumento de 129 páginas que a la comunidad matemática le tomó meses revisar a mano en una forma que un ordenador puede verificar línea por línea. El matemático Kevin Buzzard, que revisó el resultado, dijo a Anthropic que era un gran paso hacia la formalización automática de la literatura matemática moderna, logrado en mucho menos tiempo del que esperaba.
Por Qué Esto Es Una Historia de Costes, No de Matemáticas
El número que importa aquí no son los 13 millones de líneas, son los 11 días. La verificación formal, la práctica de demostrar que una pieza de matemáticas o de software es correcta en lugar de solo probarla y confiar, siempre ha sido lenta y cara de hacer a mano, y formalizar un resultado de este tamaño le había costado hasta ahora años de trabajo a equipos especializados. Ese coste es precisamente la razón por la que tan poco software crítico para la seguridad en el mundo lleva una demostración formal de corrección, y un sistema automatizado capaz de un trabajo comparable en menos de dos semanas cambia la cuenta para cualquier empresa de ingeniería europea que certifica sistemas bajo normas como la ISO 26262 para automóviles o la DO-178C para aviones, donde los métodos formales ya se usan pero se racionan por su precio.
El propio informe de Anthropic es franco sobre la tasa de fallos detrás de esa cifra llamativa: cerca del 7 por ciento del código no repetitivo provino de intentos fallidos, descartados en el camino hacia la demostración final. Eso es una parte normal de cómo siempre ha avanzado la verificación formal, sea máquina o humano, pero merece decirse con claridad, porque un éxito de 13 millones de líneas invita a la impresión contraria.
El Límite Que Nadie Debería Saltarse
Claude formalizó una demostración existente, no descubrió una nueva, y esa diferencia importa más que el logro en sí en cuanto alguien intenta apoyar peso de ingeniería sobre ella. El último teorema de Fermat funcionó como demostración precisamente porque los matemáticos ya llevaban tres décadas de acuerdo sobre cómo era la demostración correcta, lo que significaba que el trabajo de Claude era traducir un argumento conocido a un lenguaje que una máquina pudiera comprobar, no decidir si el argumento era correcto en primer lugar.
Un caso de seguridad para un sistema de frenos o un protocolo criptográfico empieza con una pregunta más difícil: qué significa correcto aquí, y lo ha especificado alguien con la precisión suficiente para que un método formal pueda comprobarlo. La formalización automatizada puede ahora reducir drásticamente la segunda mitad de ese problema. No cambia nada de la primera mitad, y cualquier organización que lea este resultado como licencia para saltarse el trabajo de especificación en lugar del de verificación lo ha malinterpretado.
Leer a continuación: 87 años cayeron ante una respuesta que cualquiera puede comprobar | Anthropic traslada tus registros a tu propia nube
