⚛️ quantum physics

Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256

Este artículo presenta una formalización agéntica del algoritmo de Shor en Lean, donde agentes de IA asistidos por revisión humana verificaron con éxito las bases matemáticas y las estimaciones de recursos lógicos para ataques cuánticos contra RSA-2048 y P-256, allanando el camino para el diseño y la verificación de algoritmos cuánticos asistidos por IA.

Autores originales: Lei Zhang, Yusheng Zhao, Hongshun Yao, Xin Wang

Publicado 2026-07-16

📖 4 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Lei Zhang, Yusheng Zhao, Hongshun Yao, Xin Wang

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina el mundo digital como una gigantesca fortaleza invisible que protege todo, desde tu cuenta bancaria hasta mensajes gubernamentales secretos. Las cerraduras de esta fortaleza son acertijos matemáticos tan complejos que, con las supercomputadoras actuales, descifrarlos tomaría más tiempo que la edad del universo. Estos acertijos son la columna vertebral de la seguridad moderna, específicamente dos tipos famosos: RSA, que se basa en la dificultad de multiplicar dos enormes números primos, y la criptografía de Curva Elíptica, que utiliza la compleja geometría de curvas dibujadas sobre una cuadrícula de números. Durante décadas, hemos creído que estas cerraduras son inquebrantables. Pero existe una "llave maestra" teórica en el mundo de la física cuántica llamada el Algoritmo de Shor. Es como una herramienta mágica que, si llegara a construirse, podría resolver estos acertijos en minutos en lugar de eones. El problema es que construir una computadora cuántica real es increíblemente difícil, y demostrar que nuestros planos matemáticos para esta "llave maestra" son realmente correctos es aún más difícil. Aquí es donde entra un nuevo tipo de trabajo detectivesco: usar la inteligencia artificial para ayudar a los matemáticos a escribir pruebas "verificadas por máquina". Piensa en ello como tener un abogado robot que lee cada uno de los pasos de un argumento legal para asegurar que no haya ni un solo error tipográfico o vacío lógico, garantizando que las matemáticas sean 100% sólidas antes de que siquiera intentemos construir la máquina.

Este artículo trata sobre un equipo de investigadores que utilizó un equipo de agentes de software (ayudantes de IA) para construir una versión rigurosa y verificada por máquina del Algoritmo de Shor, específicamente para romper dos de las cerraduras digitales más comunes del mundo: RSA-2048 y P-256. No se limitaron a adivinar cómo funcionaría; usaron IA para leer artículos científicos, escribir código en un lenguaje llamado Lean y luego hicieron que una computadora verificara cada paso lógico para asegurar que las matemáticas se sostengan. Su objetivo era crear un "plano" que demuestre exactamente cuántos recursos necesitaría una computadora cuántica para romper estas cerraduras específicas.

Para la cerradura RSA-2048, que protege gran parte de la infraestructura actual de Internet, el plano formalizado del equipo muestra que una computadora cuántica necesitaría unos 6,190 qubits lógicos (la versión cuántica de los bits de computadora) y tendría que realizar la asombrosa cantidad de 8.1 mil millones de puertas Toffoli (un tipo específico de operación lógica cuántica). Si ejecutaras este proceso tres veces seguidas para estar seguro, la profundidad total del circuito sería de 6.42 mil millones de pasos. Las matemáticas demuestran que este método encontraría con éxito la clave secreta al menos 2 de cada 3 veces.

Para la cerradura P-256, que se utiliza en muchos sitios web seguros y firmas digitales, los requisitos son aún más intensos. Su prueba formalizada indica que romper esta cerradura requeriría 2,330 qubits lógicos y una masiva cantidad de 126 mil millones de puertas Toffoli, con una profundidad de circuito de 116 mil millones de pasos. Al igual que con RSA, el algoritmo está probado para tener éxito con una probabilidad de al menos 2/3. Curiosamente, una vez que la computadora cuántica realiza su pesado trabajo, la parte humana (o de la computadora clásica) del trabajo es sorprendentemente pequeña, requiriendo solo 7 pasos aritméticos simples para terminar la tarea.

Lo que hace que este trabajo sea especial no son solo los números, sino cómo los obtuvieron. En lugar de que un humano escribiera un largo artículo y esperara que nadie encontrara un error, utilizaron un sistema "agéntico". Los agentes de software actuaron como investigadores junior: buscaron material de origen, desglosaron afirmaciones complejas en piezas diminutas, escribieron el código en Lean e incluso intentaron corregir errores en las pruebas. Los humanos revisaron la lógica científica, mientras que la computadora verificó el código. El resultado es una biblioteca de matemáticas que es "verificada por máquina", lo que significa que una computadora ha verificado cada eslabón en la cadena de la lógica.

El artículo es cuidadoso en señalar que esto es una victoria teórica, no una práctica. No han construido la computadora cuántica todavía, ni han descifrado realmente una clave RSA-2048 real. En cambio, han construido la "prueba de concepto" definitiva que dice: "Si alguna vez construimos una computadora cuántica con estos recursos específicos, así es exactamente como romperá estas cerraduras, y aquí está la garantía matemática de que funcionará". También aclaran que sus números se basan en recursos "lógicos", que son los requisitos idealizados antes de añadir la realidad desordenada de corregir los errores causados por el ruido en la máquina. Este trabajo no significa que sus contraseñas estén seguras mañana, pero sí significa que, si alguna vez obtenemos el hardware cuántico, tendremos un mapa perfectamente verificado que muestra exactamente cómo usarlo para romper las cerraduras digitales más comunes del mundo.

Resumen Técnico: Construcción del Algoritmo de Shor en Lean

Planteamiento del Problema
El artículo aborda el desafío de verificar formalmente los fundamentos matemáticos, los comportamientos de los circuitos y las estimaciones de recursos del algoritmo de Shor y sus variantes, centrándose específicamente en el criptoanálisis de RSA-2048 y la curva elíptica P-256. Si bien los esfuerzos de verificación formal existentes han cubierto partes del algoritmo de Shor (como la búsqueda del orden o las operaciones unitarias abstractas), existe una falta de desarrollos verificados por máquina que integren la cadena completa: desde la reducción del problema criptográfico y el análisis de probabilidad hasta los circuitos aritméticos reversibles y la contabilidad concreta de recursos lógicos. Los autores pretenden cerrar esta brecha proporcionando un marco unificado, verificado por máquina, en el probador de teoremas Lean que conecte las afirmaciones criptográficas de alto nivel con el recuento de puertas de bajo nivel y las probabilidades de éxito.

Metodología: Formalización Agéntica
El trabajo emplea un flujo de trabajo de "formalización agéntica". En este proceso, agentes de software asisten en el desarrollo formal mediante:

Análisis de Fuentes: Recuperación y análisis de la literatura científica relevante (específicamente [Quantum 5, 433] y [ASIACRYPT 2017, 241–270]).
Descomposición y Codificación: Desglose de las afirmaciones científicas en obligaciones matemáticas y computacionales, y posterior generación de código y pruebas en Lean.
Reparación e Iteración: Los agentes proponen revisiones para corregir errores de prueba.
Revisión Humana: Los autores humanos revisan las afirmaciones científicas, la alineación con las fuentes y las declaraciones formales resultantes.
Verificación por Máquina: El núcleo (kernel) de Lean verifica todas las pruebas aceptadas contra las definiciones y suposiciones importadas.

Este flujo de trabajo se apoya en el ecosistema de Lean, incluyendo Mathlib para matemáticas generales, CSLib para fundamentos de ciencias de la computación y Lean-QIT para la teoría de la información cuántica de dimensión finita. La biblioteca resultante utiliza nombres estables y ubicaciones de módulos para permitir que los agentes y los investigadores localicen, inspeccionen las dependencias y reutilicen los componentes verificados.

Contribuciones Clave
El artículo presenta dos aplicaciones principales de formalización dentro del ecosistema Lean:

Factorización RSA-2048:
- Formaliza la reducción de la factorización de enteros a la búsqueda del orden.
- Desarrolla circuitos de aritmética modular reversible (suma, multiplicación, exponenciación) basados en la construcción de Vedral–Barenco–Ekert.
- Implementa la ruta de Ekerå–Håstad para logaritmos discretos cortos, lo que ofrece una base de circuito lógico específica para RSA-2048.
- Combina estos elementos para producir una declaración verificada por máquina respecto a la recuperación de factores primos.
Recuperación de Escalar P-256:
- Formaliza el problema del logaritmo discreto de curva elíptica (ECDLP) sobre el cuerpo primo $\mathbb{F}_p$ .
- Construye aritmética reversible para el cuerpo primo, incluyendo la inversión de Montgomery–Kaliski y la división.
- Implementa operaciones de puntos de curva elíptica reversibles (suma y duplicación) y la multiplicación escalar mediante sumas de puntos controladas.
- Proporciona el primer desarrollo conocido en Lean que ofrece una declaración de recuperación de escalar de P-256 con un límite de éxito cuantitativo y valores de recursos lógicos.

Resultados Clave
La formalización produce dos teoremas principales con perfiles de recursos explícitos y garantías de éxito:

Teorema 1 (RSA-2048): Existe un algoritmo cuántico que devuelve un factor $d \in \{p, q\}$ con una probabilidad de al menos $2/3$ . El perfil de recursos para tres intentos secuenciales (para alcanzar el umbral de éxito) incluye:
- $6.19 \times 10^3$ qubits lógicos.
- $8.1 \times 10^9$ puertas Toffoli.
- $6.42 \times 10^9$ profundidad máxima de circuito.
- $3.69 \times 10^4$ operaciones aritméticas clásicas para la recuperación.
Teorema 2 (P-256): Existe un algoritmo cuántico que devuelve el escalar privado $m$ con una probabilidad de al menos $2/3$ . El perfil de recursos para una ejecución incluye:
- $2.33 \times 10^3$ qubits lógicos.
- $1.26 \times 10^{11}$ puertas Toffoli.
- $1.16 \times 10^{11}$ profundidad máxima de puertas Toffoli.
- 7 operaciones clásicas para la recuperación directa.

El artículo compara estos resultados con análisis asintóticos previos y estimaciones a nivel de puertas, señalando que la formalización en Lean proporciona umbrales de éxito explícitos y recuentos de operaciones clásicas que antes estaban ausentes o eran menos rigurosos en contextos verificados por máquina.

Significancia y Reivindicaciones
Los autores afirman que este trabajo representa un paso significativo hacia el diseño y la verificación de algoritmos cuánticos asistidos por IA. Al crear una capa matemática reutilizable donde la teoría de números, los límites de probabilidad, los circuitos reversibles y las fórmulas de recursos comparten un único lenguaje de prueba, la biblioteca permite a los investigadores:

Recuperar teoremas intermedios e inspeccionar sus dependencias.
Comparar formulaciones relacionadas y ensamblar componentes verificados en nuevos análisis.
Mantener un rastro desde las afirmaciones finales hasta las premisas matemáticas.

El artículo establece explícitamente que este es el primer desarrollo en Lean que proporciona una declaración de recuperación de escalar de P-256 con límites de éxito cuantitativos y valores de recursos lógicos. Posiciona este trabajo como una base para un criptoanálisis cuántico más amplio verificado por máquina.

Limitaciones y Trabajo Futuro
El artículo es modesto en cuanto a su alcance. Observa que:

Los perfiles de recursos son lógicos y no tienen en cuenta el ruido de los circuitos, la corrección de errores cuánticos, la producción de estados mágicos o la programación de qubits físicos.
Las declaraciones de aplicación final dependen actualmente de supuestos explícitos importados de la literatura (por ejemplo, recuentos de recursos específicos de las referencias [21] y [7]), en lugar de derivarse enteramente de una única ejecución de circuito formal partiendo de entradas públicas.
Se requiere trabajo futuro para construir ejecuciones completas a partir de entradas públicas (módulo $N$ o punto público $Q$ ) y para extender el análisis de recursos a arquitecturas tolerantes a fallos y familias de circuitos optimizados.

Más como este