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

Technical Summary: Building Shor's Algorithm in Lean

Problem Statement
The paper addresses the challenge of formally verifying the mathematical foundations, circuit behaviors, and resource estimates of Shor's algorithm and its variants, specifically targeting the cryptanalysis of RSA-2048 and the elliptic curve P-256. While existing formal verification efforts have covered portions of Shor's algorithm (such as order finding or abstract unitary operations), there is a lack of machine-checked developments that integrate the full chain: from cryptographic problem reduction and probability analysis to reversible arithmetic circuits and concrete logical resource accounting. The authors aim to bridge this gap by providing a unified, machine-checked framework in the Lean theorem prover that connects high-level cryptographic claims with low-level gate counts and success probabilities.

Methodology: Agentic Formalization
The work employs an "agentic formalization" workflow. In this process, software agents assist in the formal development by:

1. Source Analysis: Retrieving and analyzing relevant scientific literature (specifically [Quantum 5, 433] and [ASIACRYPT 2017, 241–270]).
2. Decomposition and Coding: Breaking down scientific claims into mathematical and computational obligations, then generating Lean code and proofs.
3. Repair and Iteration: Agents propose revisions to fix proof errors.
4. Human Review: Human authors review the scientific claims, source alignment, and the resulting formal statements.
5. Machine Checking: The Lean kernel verifies all accepted proofs against the imported definitions and assumptions.

This workflow relies on the Lean ecosystem, including Mathlib for general mathematics, CSLib for computer science foundations, and Lean-QIT for finite-dimensional quantum information theory. The resulting library uses stable names and module locations to allow agents and researchers to locate, inspect dependencies, and reuse verified components.

Key Contributions
The paper presents two primary application-level formalizations within the Lean ecosystem:

1. RSA-2048 Factorization:

   • Formalizes the reduction of integer factorization to order finding.
   • Develops reversible modular arithmetic circuits (addition, multiplication, exponentiation) based on the Vedral–Barenco–Ekert construction.
   • Implements the Ekerå–Håstad route for short discrete logarithms, which offers a specific logical-circuit baseline for RSA-2048.
   • Combines these to produce a machine-checked statement regarding the recovery of prime factors.

2. P-256 Scalar Recovery:

   • Formalizes the elliptic-curve discrete logarithm problem (ECDLP) over the prime field $\mathbb{F}_p$.
   • Constructs reversible arithmetic for the prime field, including Montgomery–Kaliski inversion and division.
   • Implements reversible elliptic-curve point operations (addition and doubling) and scalar multiplication via controlled point additions.
   • Provides the first known Lean development to give a machine-checked P-256 scalar-recovery statement with a quantitative success bound and logical resource values.

Key Results
The formalization yields two main theorems with explicit resource profiles and success guarantees:

• Theorem 1 (RSA-2048): A quantum algorithm exists that returns a factor $d \in \{p, q\}$ with probability at least $2/3$. The resource profile for three sequential attempts (to achieve the success threshold) includes:

  • $6.19 \times 10^3$ logical qubits.
  • $8.1 \times 10^9$ Toffoli gates.
  • $6.42 \times 10^9$ maximal circuit depth.
  • $3.69 \times 10^4$ classical arithmetic operations for recovery.

• Theorem 2 (P-256): A quantum algorithm exists that returns the private scalar $m$ with probability at least $2/3$. The resource profile for one run includes:

  • $2.33 \times 10^3$ logical qubits.
  • $1.26 \times 10^{11}$ Toffoli gates.
  • $1.16 \times 10^{11}$ maximal Toffoli-gate depth.
  • 7 classical operations for direct recovery.

The paper compares these results against prior asymptotic analyses and gate-level estimates, noting that the Lean formalization provides explicit success thresholds and classical operation counts that were previously absent or less rigorous in machine-checked contexts.

Significance and Claims
The authors claim this work represents a significant step toward AI-assisted design and verification of quantum algorithms. By creating a reusable mathematical layer where number theory, probability bounds, reversible circuits, and resource formulas share a single proof language, the library enables researchers to:

• Retrieve intermediate theorems and inspect their dependencies.
• Compare related formulations and assemble checked components into new analyses.
• Maintain a trace from final claims back to mathematical premises.

The paper explicitly states that this is the first Lean development to provide a machine-checked P-256 scalar-recovery statement with quantitative success bounds and logical resource values. It positions the work as a foundation for broader machine-checked quantum cryptanalysis.

Limitations and Future Work
The paper is modest regarding its scope. It notes that:

• The resource profiles are logical and do not account for circuit noise, quantum error correction, magic state production, or physical qubit scheduling.
• The final application-level theorems currently rely on explicit assumptions imported from literature (e.g., specific resource counts from Ref [21] and [7]) rather than deriving them entirely from a single formal circuit execution starting from public inputs.
• Future work is required to construct full executions from public inputs (modulus $N$ or public point $Q$) and to extend resource analysis to fault-tolerant architectures and optimized circuit families.