La comunidad matemática observó con interés el anuncio de Anthropic sobre la primera formalización completa y verificable por computadora del último teorema de Fermat. La empresa informó que su modelo Claude produjo en once días una demostración íntegra en Lean (un lenguaje diseñado para comprobación automática de demostraciones matemáticas), con cerca de 13 millones de líneas de código y más de 29.000 teoremas auxiliares, siguiendo la estructura del razonamiento presentado por Andrew Wiles en 1995 y posteriormente detallado por Henri Darmon, Fred Diamond y Richard Taylor.
El teorema, formulado por Pierre de Fermat en el siglo XVII, sostiene que no existen enteros positivos que cumplan la ecuación aⁿ + bⁿ = cⁿ para exponentes mayores que 2. Aunque la demostración de Wiles es aceptada desde hace décadas, nunca había sido traducida por completo a un formato que permitiera a una computadora verificar cada paso sin interpretación humana. La formalización realizada por Claude apunta precisamente a ese objetivo: transformar una demostración ya establecida en una cadena lógica exhaustiva y mecánicamente comprobable.
Especialistas citados por medios académicos, como Alex Kontorovich de la Universidad de Rutgers y Kevin Buzzard del Imperial College London, destacaron la magnitud del trabajo y señalaron que la velocidad del proceso supera las proyecciones de iniciativas comunitarias previas. Según análisis publicados en revistas científicas, la formalización matemática es un campo en expansión debido al creciente interés por validar demostraciones complejas con mayor rigor, especialmente en áreas donde el volumen de dependencias puede exceder la capacidad humana de revisión detallada.
El proyecto de Anthropic se suma a un contexto más amplio en el que distintas empresas tecnológicas exploran el uso de IA en investigación científica. Aunque la formalización del teorema de Fermat no modifica la demostración original, sí ofrece un ejemplo concreto de cómo la automatización puede intervenir en tareas de verificación que tradicionalmente implicaban un costo elevado en tiempo y recursos. Para la comunidad matemática, el resultado representa una referencia sobre el potencial de estas herramientas en proyectos de gran escala y en la consolidación de repositorios formales que faciliten futuras investigaciones.
Fuente: WEB
