Inteligencia Artificial Edición diaria
INTELIGENCIA ARTIFICIAL VERIFICACIÓN
Claude no ha vuelto a demostrar Fermat: ha industrializado su comprobación
Anthropic afirma que un sistema de agentes trabajó durante once días para producir la primera formalización completa del Último Teorema de Fermat en Lean. El resultado no descubre matemáticas nuevas, pero convierte una demostración monumental en un objeto que un verificador puede aceptar o rechazar paso a paso.
El titular invita al equívoco: Claude «resolvió» un misterio de 350 años. En realidad, el misterio quedó resuelto en 1995 con la prueba de Andrew Wiles y Richard Taylor. Lo nuevo es otra cosa, menos romántica y quizá más decisiva para la etapa que empieza: un modelo generalista ha convertido una ruta de aquella prueba en código Lean que un núcleo lógico pequeño puede revisar mecánicamente.
La diferencia importa. Una demostración escrita para matemáticos puede omitir pasos que la comunidad considera evidentes, apoyarse en convenciones compartidas y exigir meses de lectura experta. Lean no concede ese margen. Cada definición, dependencia e inferencia debe expresarse con precisión suficiente para que el sistema compruebe la cadena completa. El valor no está en que la IA suene convincente, sino en que su salida queda sometida a un criterio externo que no negocia con la retórica.
De una prueba histórica a una fábrica de certificados
El experimento de Anthropic muestra hasta qué punto esa traducción puede escalar. Durante once días, decenas de agentes colaboraron para definir conceptos, resolver resultados intermedios y ensamblar niveles sucesivos de la demostración. El proceso produjo unos trece millones de líneas de Lean y 30.300 teoremas auxiliares; 29.500 terminaron en la prueba final. La magnitud es reveladora: el artefacto supera en más de cinco veces el tamaño de Mathlib, la principal biblioteca comunitaria sobre la que se apoya.
La coordinación fue tan importante como el modelo. Los primeros intentos perdieron el estado del proyecto y dejaron de colaborar con eficacia. El equipo cambió entonces a Prove2Me, una plataforma que representa los teoremas como un grafo dirigido, separa en archivos distintos los enunciados y las pruebas y mantiene descripciones en lenguaje natural para favorecer la búsqueda y la reutilización. Con ese andamiaje y un sistema multiagente basado en Claude Code, el proyecto consumió cerca de seis mil millones de tokens de salida de un modelo interno comparable, según la empresa, a Claude Fable 5.1.
La ruta matemática tampoco nació del vacío. Claude siguió una versión simplificada de la prueba de Wiles expuesta por Henri Darmon, Fred Diamond y Richard Taylor, y reutilizó trabajo de iniciativas comunitarias previas. La intervención humana se concentró en instrucciones de alto nivel y prioridades, pero la arquitectura intelectual, las bibliotecas y el criterio de qué debía formalizarse procedían de años de trabajo humano. Kevin Buzzard, impulsor de la formalización de Fermat en Imperial College, revisó el resultado, y el código se publicó para su inspección.
Por eso el avance es más relevante para la verificación que para la creatividad matemática. Si los modelos generan cada vez más conjeturas, pruebas, programas y políticas, el cuello de botella será comprobarlas. Una salida en lenguaje natural obliga a confiar en el modelo o a rehacer su trabajo; una salida acompañada de un certificado formal puede someterse a un comprobador independiente. La misma lógica se extiende más allá de los teoremas: reglas de autorización, protocolos, algoritmos financieros o componentes de seguridad pueden describirse como propiedades que el software debe satisfacer.
Pero «verificado» no significa «verdadero en todos los sentidos». Lean comprueba que la conclusión se sigue de los axiomas, definiciones y enunciados introducidos. Si la especificación representa mal el problema, la prueba puede ser impecable y el sistema real seguir fallando. Tampoco conocemos aún el coste total de reproducir el proyecto, la facilidad para comprimir un artefacto gigantesco ni cuánto trabajo humano hará falta para convertirlo en una exposición legible. El propio experimento reconoce que una parte de los intentos fallidos sobrevivió en la versión final y que la formalización es mucho más extensa de lo necesario.
El cuello de botella se desplaza a la revisión
Precisamente ahí está el cambio de cuello de botella. Si los modelos empiezan a producir con rapidez conjeturas y pruebas extensas, la revisión humana no puede crecer al mismo ritmo. Una versión formal actúa como control de integridad: obliga a declarar supuestos, detecta huecos y permite reutilizar componentes sin confiar sólo en reputación o intuición. No elimina la necesidad de juicio matemático —elegir problemas, interpretar resultados y explicar por qué una idea es fértil—, pero puede reducir la carga mecánica que hoy consume meses de referees y equipos de formalización.
La aplicación empresarial no es convertir cualquier contrato en un teorema mañana. Sí lo es adoptar el principio: las respuestas de un agente deben terminar en verificadores independientes cuando el coste de un error es alto. En software puede ser una batería de pruebas y un analizador estático; en finanzas, reglas contables deterministas; en operaciones, límites que el agente no puede reescribir. El éxito de Claude en Lean es menos una invitación a delegar la verdad que un ejemplo de cómo envolver generación probabilística con comprobación rigurosa.
Etiquetas
- Anthropic
- Claude
- Lean
- Verificación formal
- Fermat
- Mathlib
BOLDERROR Edición diaria Rubén Campoy