Prueba formal y salidas verificables: cuando el verificador zanja la cuestión

Un agente entrega una respuesta. Otro agente la revisa. Ambos coinciden. Aun así, la conclusión puede ser errónea porque comparten modelos, contexto, supuestos o fallos similares.

El anuncio de Anthropic sobre la formalización del último teorema de Fermat ofrece un caso poco común: verificadores formales pudieron rechazar o aceptar el artefacto generado por IA sin confiar en la elocuencia del modelo.

Estado: Evidence Brief aprobado para publicación. Este texto analiza un artefacto público y propone un patrón de arquitectura. No afirma que Trustyu Forge haya reproducido el experimento ni que este diseño esté implementado u operando en todos sus productos.

Alcance correcto de la afirmación

El 4 de septiembre de 2026, Anthropic informó que su sistema multiagente Prove2Me formalizó en Lean una prueba existente del último teorema de Fermat. La publicación de Anthropic describe 11 días de trabajo, decenas de agentes, aproximadamente 6 mil millones de tokens de salida, más de 13 millones de líneas de Lean producidas durante el proceso y 29.511 declaraciones utilizadas en la prueba final.

La formulación precisa importa: los agentes no descubrieron el teorema ni una nueva prueba matemática. Convirtieron una exposición simplificada de la prueba de Wiles y Taylor-Wiles en una cadena formal verificable. El repositorio público fija Lean 4.33.1 y Mathlib v4.33.0, proporciona instrucciones de compilación y expone los artefactos bajo licencia Apache-2.0.

Estas cifras no informan del costo financiero total, la productividad humana equivalente ni el rendimiento en otros dominios. Miden el proceso y el artefacto en este caso.

Cuatro capas de verificación

1. El cuerpo formal

Lean transforma cada paso en términos que deben satisfacer el sistema de tipos. La respuesta final no se acepta porque parezca correcta: debe ser reconstruida por el kernel.

2. El kernel de Lean

El repositorio informa de una compilación de 60.475 módulos. El kernel verificó la cadena utilizando tres axiomas estándar. La superficie de confianza es menor que toda la pila que produjo el código, pero no es cero: incluye el kernel, las versiones fijadas, la cadena de build y el entorno.

3. El Comparator

O Comparator compara teoremas de Lean hasta la igualdad definicional. En este caso, se utilizó para comprobar si la declaración final corresponde al teorema esperado en Mathlib y si coincide la lista de axiomas. Esto evita un falso positivo común en la generación formal: demostrar un enunciado similar pero más débil o diferente.

4. Un kernel independiente

Según Anthropic y el repositorio, Nanoda —un verificador en Rust independiente del kernel de Lean— comprobó 1.052.234 declaraciones sin errores. Fueron necesarios cuatro pequeños patches, descritos como no debilitadores del sistema de tipos. Esta salvedad debe permanecer junto a la afirmación; “verificador independiente” no significa reproducción sin adaptación.

Kevin Buzzard, profesor del Imperial College London y líder de un proyecto relacionado de formalización, relata en el Xena Project haber compilado el código y ejecutado el Comparator con éxito. Es una corroboración externa relevante. También existe contexto de relación: Anthropic proporcionó al proyecto académico acceso a una máquina de 500 GB.

Proof-carrying output para agentes

En seguridad de software, proof-carrying code describe código acompañado por evidencia verificable de propiedades. El patrón puede generalizarse con cuidado para los agentes: una salida que lleva prueba incluye el resultado, las condiciones en las que se produjo y un artefacto que un verificador independiente puede reconstruir.

Una respuesta de texto no se convierte en prueba solo por incluir una justificación. Para ser proof-carrying, la evidencia debe tener una semántica definida, aceptar el rechazo y reducir la confianza depositada en el generador.

spec versionada
      ↓
gerador probabilístico ──→ artefato candidato
                               ↓
                    verificador independente
                         ↙           ↘
                    rejeita        aceita
                       ↓              ↓
              evidência de falha   receipt assinado
                       └──────→ decisão humana/runtime

Un contrato mínimo de salida verificable

El contrato debe sobrevivir a sesiones, modelos y equipos. Los entornos aislados, el estado explícito y la evidencia duradera son propiedades del harness alrededor del agente, no cualidades mágicas del modelo. Ayudan a hacer observables los fallos, pero no demuestran automáticamente que un producto sea seguro o esté listo para operar. [HARNESS31-C2]

Qué enseña Prove2Me sobre orquestación

O paper de Prove2Me describe un sistema neurosimbólico que organiza objetivos como un grafo dirigido acíclico, paraleliza subtareas, busca y reutiliza lemas y separa la proposición de declaraciones de la construcción de pruebas.

Este diseño contiene cuatro lecciones transferibles:

1. La dependencia es una entidad del sistema. Las subtareas solo avanzan cuando se cumplen sus prerrequisitos.
2. El estado es compartido y versionado. Los agentes no trabajan solo a partir de resúmenes conversacionales.
3. El verificador crea feedback objetivo. Los fallos vuelven al ciclo sin requerir una evaluación subjetiva del propio generador.
4. Los intentos fallidos son evidencia. Anthropic informa de enfoques anteriores que no escalaron; el resultado dependió del scaffolding y la descomposición, no solo de una mayor capacidad del modelo.

Dónde encaja este patrón — y dónde no

Proof-carrying output es especialmente útil cuando el dominio ofrece invariantes verificables:

• compilación, tipos, pruebas y propiedades de software;
• conciliación contable y conservación de totales;
• aplicación de políticas y límites de acceso;
• transformaciones de datos con contratos de esquema;
• cálculos reproducibles y trazas regulatorias;
• configuraciones que pueden evaluarse mediante policy-as-code.

El patrón es más limitado cuando el resultado depende del gusto, la negociación, el contexto social, el pronóstico humano o categorías jurídicas abiertas. En esos casos, la evidencia estructurada sigue siendo útil, pero no elimina el juicio, la disputa interpretativa ni la responsabilidad profesional.

Costo de reproducción y límite operativo

O repositorio informa que el build completo generó cerca de 67 GB en la carpeta .lake, utilizó aproximadamente 220 GB para archivos C temporales, tardó 5 horas y 32 minutos con 96 trabajos paralelos y alcanzó un pico de memoria de 153 GB. El Comparator tardó aproximadamente 15 horas y llegó a 230 GB.

Esto demuestra que la verificabilidad también consume ingeniería e infraestructura. Anthropic no publicó el costo total del experimento. Seis mil millones de tokens no deben convertirse en precio sin conocer modelos, descuentos, caché, intentos internos e infraestructura. Para el producto, el objetivo no es maximizar la prueba, sino elegir evidencia proporcional a la consecuencia y al riesgo.

Gate técnico antes del release

Un equipo puede utilizar este gate para un flujo crítico:

1. ¿El requisito está versionado y tiene condiciones explícitas de rechazo?
2. ¿El resultado material —no solo el texto— es verificable?
3. ¿El verificador es independiente del generador en la dimensión de fallo relevante?
4. ¿La entrada, la salida, las versiones y las evidencias están vinculadas mediante digests?
5. ¿Fallo, resultado no concluyente y timeout son estados distintos del éxito?
6. ¿La autoridad de release está separada de la producción y la verificación?
7. ¿Se midieron el costo y la latencia de la verificación en el p95?
8. ¿Existe fallback y el error permanece contenido y reversible?

Un gate aprobado no es evidencia de producción observada. Es una autorización delimitada para la versión y el alcance evaluados.

Limitaciones, contrapuntos y conflictos

• Anthropic es la fuente principal y desarrolladora del sistema; tiene un interés comercial en el resultado.
• El repositorio abierto, los kernels y la evaluación de Buzzard refuerzan la afirmación técnica, pero no constituyen una auditoría financiera ni una reproducción por múltiples grupos independientes.
• Buzzard considera que el trabajo aporta poco a las matemáticas conocidas y mucho a la autoformalización; su análisis también tiene lugar en un ecosistema que recibió infraestructura de Anthropic.
• El dominio matemático permite la verificación formal. La misma garantía no se transfiere a decisiones abiertas.
• Las líneas, los tokens y el número de declaraciones miden volumen, no valor de forma aislada.
• No se divulgaron el costo total, la energía consumida ni la distribución de los intentos fallidos.

Fuentes y contexto editorial

1. Anthropic — Formalizing Fermat's Last Theorem in Lean. Fuente primaria del proveedor, publicada el 04/09/2026.
2. Anthropic — repositorio fermats-last-theorem. Código, versiones, instrucciones, métricas de build y licencia.
3. Xena Project — FLT: Anthropic has beaten me to it. Corroboración y contrapunto de Kevin Buzzard.
4. Prove2Me. Descripción del sistema neurosimbólico y de la orquestación.
5. Lean Comparator. Implementación del comparador utilizado en la verificación.

Nota editorial y de responsabilidad

Este texto combina hechos atribuidos a las fuentes con el análisis y la propuesta técnica del autor. Los puntos de vista personales y profesionales no son hechos comprobados; se indican datos, denominadores, límites y conflictos cuando están disponibles. El contenido es informativo y no sustituye una evaluación técnica, matemática, jurídica, financiera o de seguridad específica. Tech Human y Trustyu operan comercialmente en áreas relacionadas. La investigación, la estructura y la redacción contaron con asistencia de IA; la revisión factual, la aprobación del autor y la publicación fueron confirmadas por Fernando Parreiras el 05/09/2026, sin revisión humana independiente adicional.

Corte de la investigación: 05/09/2026. Estado editorial: publicación especial extraordinaria autorizada para el 05/09/2026 a las 19:21 BRT.