Capital de Tokens
¿Qué significa formalizar las matemáticas? Fermat, Lean y la diferencia entre rigor humano y prueba verificable
La noticia suena extraña la primera vez que se escucha: Anthropic anunció que Claude produjo una prueba completa y comprobada por computadora del Último Teorema de Fermat en Lean.
Y aparece inmediatamente una pregunta razonable:
¿Qué significa “formalizar” un teorema? ¿Las matemáticas no son formales en sí mismas?
La respuesta corta es: las matemáticas modernas son rigurosas, pero la mayor parte de la matemática que leen y escriben los humanos no está expresada como una prueba formal completa para una máquina.
Ese matiz parece pequeño, pero cambia mucho.
Una demostración publicada puede ser perfectamente válida para matemáticos expertos y, al mismo tiempo, contener cientos o miles de pasos que una persona competente reconstruye mentalmente sin necesidad de verlos escritos.
Un asistente de pruebas como Lean no hace eso.
No interpreta intención. No acepta “es evidente”. No rellena un lema omitido porque probablemente era lo que el autor quería decir.
Necesita que el argumento quede expresado con suficiente precisión para que un pequeño verificador —el kernel— pueda comprobar cada paso conforme a reglas lógicas explícitas.
Ese es el salto de matemática rigurosa para humanos a matemática formalizada para verificación mecánica.
Tres niveles que conviene separar
Podemos pensar en tres niveles.
1. Intuición matemática
Es la etapa en la que alguien sospecha que una afirmación debe ser verdadera y tiene una explicación conceptual de por qué.
Por ejemplo:
“Parece imposible que tres potencias de este tipo encajen para exponentes mayores que dos.”
Eso puede guiar una investigación, pero no es una demostración.
2. Prueba rigurosa para humanos
Aquí ya existe una cadena de argumentos que especialistas pueden revisar.
Sin embargo, esa cadena utiliza convenciones compartidas, notación, experiencia y una enorme biblioteca mental de resultados previos.
Un paper puede decir cosas como:
“Aplicando el argumento estándar…”
“Por el lema anterior, el resultado se sigue inmediatamente.”
“El otro caso es análogo.”
Para un lector experto, esas frases pueden ser completamente aceptables.
El autor no tiene que volver a definir qué es un número natural, cómo funciona la suma o qué reglas lógicas permiten sustituir iguales por iguales.
La comunidad comparte ese contexto.
3. Prueba formal
Una prueba formal elimina esa dependencia de interpretación humana en el proceso de verificación.
Las definiciones deben existir dentro del sistema. Las hipótesis deben estar disponibles explícitamente. Los teoremas usados deben haber sido demostrados o aceptados como parte de la base axiomática. Cada transformación tiene que ser legal bajo las reglas del sistema.
En lugar de:
“Esto se sigue por un argumento estándar.”el verificador necesita algo conceptualmente más parecido a:
hipótesis
↓
lema A
↓
lema B
↓
regla lógica válida
↓
conclusiónLa computadora no tiene que “estar de acuerdo” con la prueba. Tiene que poder reproducir su validez paso a paso.
Entonces, ¿las matemáticas no son ya formales?
En fundamentos de la matemática, sí existe una idea muy precisa de sistema formal: símbolos, axiomas y reglas de inferencia.
En principio, una gran parte de la matemática moderna puede expresarse dentro de sistemas formales apropiados.
Pero eso no significa que cada libro, paper o pizarra esté escrito de esa manera.
Los matemáticos trabajan en un nivel de abstracción mucho más cómodo para seres humanos.
Podemos hacer una analogía con programación.
Un arquitecto de software puede dibujar:
cliente → API → base de datosEso describe correctamente una arquitectura, pero no es un programa ejecutable.
Para ejecutarlo hay que precisar tipos, interfaces, condiciones de error, formatos de datos, dependencias y miles de detalles más.
Con una prueba matemática ocurre algo parecido.
Una demostración humana puede describir correctamente el camino lógico sin enumerar cada micro-paso necesario para que una máquina lo ejecute como una derivación formal.
Formalizar es hacer ejecutable el rigor.
Un ejemplo diminuto: 1 + 1 = 2
Para nosotros:
[ 1 + 1 = 2 ]
es inmediato.
Pero un sistema formal necesita tener alguna representación de:
- los números naturales;
- el número
1; - el número
2; - la operación de suma;
- la igualdad;
- las reglas que permiten reducir o demostrar esa expresión.
En un asistente moderno gran parte de esa infraestructura ya viene construida en bibliotecas, por lo que el usuario no empieza desde cero.
Aun así, el principio permanece: nada puede depender de que el verificador “entienda lo que quisimos decir”.
Fermat hace visible la diferencia
El Último Teorema de Fermat afirma, en una formulación habitual, que para enteros positivos y exponentes mayores que dos no existen soluciones a:
[ a^n + b^n = c^n ]
La afirmación cabe en una línea.
La demostración no.
Andrew Wiles, junto con el trabajo posterior con Richard Taylor, resolvió el problema en los años noventa usando matemáticas profundas relacionadas con curvas elípticas, formas modulares, representaciones de Galois y teoría de números.
Para matemáticos, esa prueba ya era una demostración rigurosa.
“Formalizar Fermat” no significa volver válida una prueba que antes era informal o dudosa.
Significa traducir una ruta matemática suficientemente completa a objetos y demostraciones que Lean pueda comprobar mecánicamente.
El propio repositorio publicado por Anthropic contiene una declaración de Lean que, simplificada visualmente, tiene esta estructura:
theorem fermat_last_theorem
(n : ℕ)
(hn : 3 ≤ n)
(a b c : ℕ)
(ha : 0 < a)
(hb : 0 < b)
(hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ nAquí ya no basta con decir “n es mayor que dos”.
El tipo de n está especificado. Las variables a, b y c están tipadas. La positividad de cada una aparece como hipótesis. La conclusión está escrita dentro del lenguaje que Lean sabe comprobar.
Y eso es solamente el enunciado.
Lo difícil es toda la red de resultados necesaria para llegar hasta él.
¿Qué comprobó exactamente Lean?
Según Anthropic, Claude trabajó en la formalización durante 11 días, en gran medida de forma autónoma, y produjo alrededor de 13 millones de líneas de Lean. El proyecto generó decenas de miles de teoremas intermedios; Anthropic reporta 30,300 demostrados durante el proceso y 29,500 utilizados en la prueba final.
La prueba publicada fue ejecutada y comprobada por el kernel de Lean.
El repositorio de Anthropic también incluye verificaciones adicionales. Su FinalCheck.lean comprueba que el teorema depende únicamente de tres axiomas estándar de Lean, y el proyecto utiliza un comparador para confirmar que el enunciado demostrado corresponde al enunciado de Fermat usado por Mathlib.
Incluso se hizo una segunda comprobación con nanoda, un kernel independiente escrito en Rust.
Esto no significa que una computadora haya alcanzado una forma metafísica de certeza absoluta.
Siempre existe una base de confianza:
axiomas
↓
reglas lógicas
↓
kernel de Lean
↓
prueba formal
↓
teoremaPero esa base es muchísimo más pequeña y explícita que pedir a seres humanos que inspeccionen manualmente millones de pasos.
La idea clave es que no tenemos que confiar en que Claude “razonó bien”.
Podemos dejar que Claude proponga millones de pasos y confiar en un verificador mucho más pequeño para aceptar únicamente los que cumplen las reglas.
El patrón poderoso: generador probabilístico + verificador determinista
Aquí aparece una conexión importante con la ingeniería de agentes.
Un modelo de lenguaje es probabilístico. Puede equivocarse. Puede intentar un camino inútil. Puede inventar una afirmación falsa.
Lean cumple otra función.
Claude propone
↓
prueba candidata
↓
Lean verifica
↙ ↘
rechazo aceptación
↓ ↓
reintento resultado válidoEso crea un bucle muy atractivo para sistemas autónomos.
El modelo no necesita ser infalible.
Necesita operar dentro de un entorno donde los errores relevantes puedan detectarse automáticamente.
Es el equivalente matemático de darle a un agente de programación compiladores, type checkers, linters y tests extremadamente fuertes.
La diferencia es que en una prueba formal el verificador puede cubrir la corrección lógica con una fuerza que los tests de software normales rara vez alcanzan.
El problema no era solamente demostrar: era coordinar
Otro aspecto interesante del trabajo de Anthropic es que los primeros intentos multiagente fallaron.
Los agentes perdían la noción del estado global del proyecto y dejaban de colaborar de forma efectiva.
La solución fue utilizar Prove2Me junto con un harness multiagente basado en Claude Code.
Prove2Me mantenía un DAG —un grafo dirigido acíclico— de teoremas y dependencias.
Conceptualmente:
Fermat
│
┌─────────┴─────────┐
│ │
teorema A teorema B
│ │
┌────┴────┐ ┌────┴────┐
│ │ │ │
lema A1 lema A2 lema B1 lema B2Cada agente podía ver qué piezas estaban listas para trabajarse, cuáles dependían de otras y qué resultados podían reutilizarse.
El grafo funcionaba como memoria externa y estructura de coordinación.
Este detalle importa más allá de las matemáticas.
En tareas largas, no basta con aumentar la ventana de contexto del modelo. El estado del trabajo debe existir fuera del modelo, en artefactos que puedan inspeccionarse, verificarse y compartir entre agentes.
Formalizar no es “explicar con más detalle”
También conviene evitar otra confusión.
Una explicación extremadamente detallada para humanos todavía puede no ser una formalización.
Podemos escribir cien páginas explicando por qué una prueba funciona y seguir usando lenguaje natural.
Una prueba formal no se define por su longitud, sino por estar codificada dentro de un sistema cuyas reglas permiten que una máquina verifique la derivación.
Por eso pueden coexistir dos documentos complementarios:
exposición humana
→ busca comprensión
prueba formal
→ busca verificabilidad mecánicaAnthropic también subraya que una formalización no debería sustituir a una buena explicación para humanos.
Las dos sirven para cosas diferentes.
¿Puede una prueba formal tener un error?
La respuesta cuidadosa es: el riesgo cambia de lugar.
Una prueba formal aceptada por Lean no debería contener un salto lógico inválido respecto a las reglas y axiomas que Lean está verificando.
Sin embargo, todavía debemos preguntar:
- ¿formalizamos el teorema correcto?;
- ¿las definiciones representan lo que creemos que representan?;
- ¿qué axiomas se usaron?;
- ¿el kernel es correcto?;
- ¿la cadena de herramientas conserva lo que dice conservar?
Por eso el proyecto de Anthropic dedica atención a comprobar el enunciado final, los axiomas utilizados y una segunda implementación del kernel.
La formalización no elimina toda epistemología.
Reduce radicalmente la cantidad de razonamiento que debemos aceptar sólo porque un humano o una IA dice que está bien.
¿Por qué esto importa ahora?
Durante décadas, la formalización matemática fue costosa porque había que convertir manualmente argumentos escritos para humanos en código de prueba extremadamente detallado.
La IA cambia la economía de ese proceso.
Si los agentes pueden encargarse de gran parte del trabajo mecánico de traducción y Lean puede verificar el resultado, aparece un pipeline nuevo:
paper / libro / idea matemática
↓
agentes de formalización
↓
Lean / Mathlib
↓
verificación automática
↓
prueba formal reutilizableEso podría tener varias consecuencias.
Detectar errores en literatura existente
Resultados que han sido aceptados durante años podrían verificarse con una profundidad que el proceso humano de revisión no siempre puede permitirse.
Revisar matemáticas producidas por IA
Si los modelos empiezan a producir más resultados novedosos, la comunidad necesita una manera escalable de comprobarlos.
La combinación IA + formalización ofrece una respuesta posible: no confiar en la prosa del modelo; exigir un artefacto que el verificador pueda comprobar.
Crear bibliotecas reutilizables
Una vez que una teoría está formalizada, otros investigadores pueden construir encima de ella sin volver a demostrar desde cero cada resultado.
Cambiar el rol del matemático
Parte del trabajo podría desplazarse desde escribir cada detalle de una prueba hacia elegir definiciones correctas, diseñar estrategias, interpretar resultados y construir explicaciones humanas útiles.
La paradoja interesante
Las matemáticas siempre han buscado rigor.
Lo nuevo no es esa aspiración.
Lo nuevo es que podemos representar ese rigor en un formato que una máquina pueda ejecutar como verificación.
Por eso la mejor respuesta a “¿las matemáticas no son formales en sí?” es:
Las matemáticas pueden fundamentarse formalmente, pero la matemática cotidiana de los humanos normalmente está escrita en un lenguaje riguroso que todavía depende de interpretación, contexto y conocimiento compartido. Formalizar es eliminar esa dependencia de la etapa de verificación.
Y el caso de Fermat muestra por qué esta distinción está dejando de ser puramente académica.
Cuando un conjunto de agentes puede producir millones de pasos y un kernel pequeño puede comprobarlos, la formalización se convierte en algo más que una técnica especializada: se vuelve una infraestructura potencial para hacer ciencia con sistemas de IA que trabajan a una escala que ningún revisor humano podría inspeccionar línea por línea.