Un modelo experimental de inteligencia artificial desarrollado por la firma estadounidense Anthropic ha completado la traducción completa a código informático de la demostración del último teorema de Fermat.
La operación, efectuada mediante el lenguaje de programación formal Lean —diseñado específicamente para la verificación lógica de enunciados matemáticos—, requirió once días de procesamiento distribuido. Durante este lapso, el sistema generó aproximadamente 13 millones de líneas de código y resolvió más de 30.000 teoremas intermedios para respaldar la estructura lógica de la prueba.
El último teorema de Fermat, formulado originalmente por el matemático francés Pierre de Fermat en 1637, plantea que la ecuación xⁿ + yⁿ = zⁿ carece de soluciones enteras positivas para cualquier exponente mayor a dos. Tras permanecer sin verificación formal durante más de tres siglos, el matemático británico Sir Andrew Wiles, con aportes posteriores de Richard Taylor, formuló la primera demostración rigurosa a mediados de la década de 1990 utilizando herramientas avanzadas de la teoría de números.
La tarea de traducir dicha argumentación humana a un formato interpretable y verificable por computadoras formaba parte de un proyecto académico liderado por el matemático Kevin Buzzard, del Imperial College de Londres, cuyo cronograma contemplaba hasta diez años de trabajo colectivo. El propio Buzzard reconoció públicamente la validez del código generado por el modelo tras auditar el archivo producido, destacando la solidez de la autoformalización.
El proceso de conversión técnica presentó desafíos iniciales. Los agentes virtuales de la firma experimentaron fallos de coordinación en sus fases preliminares. Para solucionar esta limitación, los investigadores de la empresa integraron la plataforma de colaboración matemática Prove2Me, desarrollada en conjunto con la Universidad de Columbia, la cual permitió mantener un mapa estructurado de las dependencias lógicas pendientes y optimizar el trabajo paralelo entre los modelos.
A pesar de la magnitud de la sintaxis producida —que supera en cinco veces el tamaño de MathLib, la principal biblioteca comunitaria de matemáticas formalizadas—, el resultado actual presenta una restricción operativa. El volumen e hiperespecificidad del código impiden su integración directa en el repositorio estándar utilizado por la comunidad científica.
El logro se enmarca en una competencia creciente dentro de la industria de la tecnología por aplicar modelos de lenguaje en la verificación de razonamientos abstractos, un campo donde competidores como OpenAI y Google DeepMind también orientan recursos para la automatización de la investigación científica. Analistas del sector y matemáticos coinciden en que, si bien el experimento no aporta descubrimientos teóricos inéditos, demuestra la viabilidad de utilizar enjambres de inteligencia artificial para auditar literatura científica extensa en tiempos reducidos.
Fuente: Anthropic
