Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256
Source: arXiv:2607.14082 · Published 2026-07-15 · By Lei Zhang, Yusheng Zhao, Hongshun Yao, Xin Wang
TL;DR
This paper addresses the formal verification and machine-checked proof of Shor's algorithm applied to two crucial cryptographic instances: factoring a 2048-bit RSA modulus (RSA-2048) and solving the discrete logarithm problem on the standardized elliptic curve P-256. The authors employ Lean, an interactive theorem prover with strong libraries in mathematics and quantum information theory, to formalize the mathematical foundations and quantum circuits underlying these attacks. They introduced an agentic formalization workflow in which software agents automatically research sources, generate Lean code, repair proofs, and humans perform scientific review. The result is a fully machine-checked end-to-end proof chain linking the cryptographic problem definitions, quantum order-finding and discrete-log reductions, reversible modular and elliptic-curve arithmetic circuits, classical postprocessing, success probability bounds, and resource accounting in terms of logical qubits, Toffoli gates, and circuit depth.
The key novel contribution is the first Lean machine-checked formalization covering concrete, quantitative logical resource estimates and explicit success probability thresholds for attacking RSA-2048 and P-256 via Shor's algorithm and variants (including the Ekerå–Håstad factoring route). The formalization rigorously composes these building blocks into application-level theorems relating public keys to the recovered private factors or scalars. For example, the RSA-2048 result shows that three sequential order-finding attempts succeed with probability ≥ 2/3 using 6190 logical qubits, 8.1×10^9 Toffoli gates, and 6.42×10^9 maximal circuit depth, plus 3.69×10^4 classical arithmetic operations. Similarly, the P-256 discrete log formalization attains ≥ 2/3 success probability with 2330 logical qubits, 1.26×10^11 Toffoli gates, 1.16×10^11 maximal Toffoli gate depth, and 7 classical operations. The work paves the way for trustworthy, machine-checked quantum cryptanalysis and AI-assisted design and verification of quantum algorithms.
Key findings
- RSA-2048 attack: quantum algorithm succeeds with probability ≥ 2/3 after three sequential attempts
- Resources for RSA-2048 factoring: 6190 logical qubits, 8.1×10^9 Toffoli gates, 6.42×10^9 maximal quantum circuit depth, 3.69×10^4 classical arithmetic operations (Theorem 1)
- P-256 discrete log attack: quantum algorithm recovers private scalar m with probability ≥ 2/3 in one run
- Resources for P-256 recovery: 2330 logical qubits, 1.26×10^11 Toffoli gates, 1.16×10^11 maximal Toffoli gate depth, 7 classical operations (Theorem 2)
- Agentic formalization workflow successfully automates source analysis, proof construction, and verification with human review to produce fully machine-checked formal statements
- Formalization covers complete chain: mathematical reductions, quantum order-finding and discrete log algorithms, reversible modular and prime-field arithmetic circuits, elliptic-curve operations, classical postprocessing, success probabilities, and resource bounds
- Lean formalization includes gate-level circuit constructions for modular exponentiation and elliptic-curve scalar multiplication, leaving no arithmetic oracles
- Formal results improve on prior work by providing explicit quantitative success probabilities, concrete resource counts, and classical operation tallies.
Threat model
The threat model assumes an adversary with the capability to run the full quantum algorithm represented as an ideal logical quantum circuit with access to a known public RSA-2048 modulus or P-256 elliptic-curve public key. The adversary has unlimited classical computational resources for post-processing but no access to side-channel or physical-layer attacks. The adversary cannot bypass quantum logical resource constraints or noise limitations, and the analysis excludes faults and physical overheads. The goal is to recover private RSA factors or P-256 scalars with a well-defined success probability.
Methodology — deep read
The paper follows a rigorous formal verification approach using the Lean theorem prover augmented with quantum information theory libraries (Lean-QIT) and automated proof assistant agents (LeanDojo). The threat model is classical: an adversary aims to break RSA-2048 or P-256 by recovering private factors/scalars from public keys using a quantum computer running Shor's algorithm or variants. The adversary's capabilities align with idealized quantum logical resource models, counting qubits, logical gates, and circuit depth, but ignoring noise and error correction overhead.
Data provenance derives primarily from classical cryptographic instances: the 2048-bit RSA modulus N = pq and the P-256 elliptic curve parameters (prime field p, base point P, order r, public key Q). The target outputs are the factors p or q for RSA, and the scalar m such that Q = [m]P for P-256. The formalization encodes these cryptographic problems as precise computational problems in Lean, with corresponding success events.
The core algorithmic architecture formalized includes Shor's order-finding algorithm via quantum phase estimation and continued fractions verification, reversible modular arithmetic circuits implementing modular addition, multiplication, and exponentiation (following Vedral–Barenco–Ekert constructions), and elliptic-curve point additions and scalar multiplications over prime fields using reversible circuits. For RSA-2048, both the textbook order-finding route and the Ekerå–Håstad short discrete-logarithm reduction are formalized. For P-256, the discrete log reduction is formalized along with layered prime-field arithmetic and elliptic-curve operations.
The training and proof development proceeded by agents parsing literature, extracting and decomposing lemmas and claims, generating Lean formal statements and proofs, and iteratively repairing failed proofs. Human reviewers validated scientific correctness, alignment to sources, and overall coherence. Machine checking via the Lean kernel ensured logical consistency and proof correctness.
Evaluation involves verifying the full proof chains in Lean, deriving explicit lower bounds on success probabilities (≥ 2/3 for both targets), and producing exact logical resource counts for qubit usage, Toffoli gate counts, and circuit depths for the quantum circuits, as well as counts of classical arithmetic recovery steps. They compare these formally verified results against prior asymptotic and gate-level estimates from the literature, showing consistency and adding formal guarantees.
Reproducibility is supported by an open-source GitHub repository (github.com/QudeLeap/Lean-QuantumAlg) containing the full Lean formalization, agent scripts, and proof libraries. The datasets are classical cryptographic key parameters public in standards. The paper provides no mention of frozen weights or machine learning models, as this is a formal methods rather than empirical ML paper.
Concretely, for one RSA-2048 factorization attempt, the phase register of 2t qubits uses quantum phase estimation; controlled modular multiplications controlled by bitwise exponents implement modular exponentiation reversibly. Intermediate qubit states are uncomputed to retain reversibility. Measurements yield integers used in continued-fraction convergents to recover the order r. Multiple such attempts are composed to amplify success probability. Similarly, the P-256 approach uses reversible prime-field arithmetic building up controlled elliptic-curve point operations and scalar multiplication. The classical recovery steps transform measured data into final secret key outputs.
In summary, the methodology tightly integrates classical cryptographic problem definitions, quantum algorithm construction at the gate/circuit level, reversible classical arithmetic circuits, success probability math, classical postprocessing, and formal proof verification into one coherent Lean framework.
Technical innovations
- Agentic formalization pipeline integrates automated source analysis, proof synthesis, and repair with human scientific review and machine-checked verification in Lean.
- Full gate-level formalization of reversible modular arithmetic and elliptic-curve arithmetic circuits, leaving no arithmetic oracles, enabling end-to-end quantum cryptanalysis proofs.
- Explicit machine-checked theorems providing concrete success probability bounds ≥ 2/3 and detailed logical resource counts for RSA-2048 factoring and P-256 discrete logarithm recovery.
- Formal linking of quantum order-finding and discrete-log algorithms with classical recovery postprocessing and resource accounting, forming a reusable mathematical and computational library for quantum cryptanalysis.
Datasets
- RSA-2048 public modulus — 2048-bit integer — standard public cryptographic modulus
- P-256 elliptic curve parameters — curves over 256-bit prime field — NIST standardized parameters
Baselines vs proposed
- Asymptotic analysis [5]: O(n) qubits, O(n^3) elementary gates vs Lean-formalized RSA-2048: 6190 qubits, 8.1×10^9 Toffoli gates
- Gate-level estimate [21]: 6190 qubits, 2.7×10^9 Toffoli gates, 2.14×10^9 measurement depth vs Lean-formalized RSA-2048: 6190 qubits, 8.1×10^9 Toffoli gates, 6.42×10^9 max circuit depth
- Approximate analysis [22]: ~1500 qubits, ~1.81×10^10 Toffoli gates vs Lean-formalized P-256: 2330 qubits, 1.26×10^11 Toffoli gates
- Gate-level estimate [7]: 2330 qubits, 1.26×10^11 Toffoli gates, 1.16×10^11 depth vs Lean-formalized P-256: identical resource counts
Figures from the paper
Figures are reproduced from the source paper for academic discussion. Original copyright: the paper authors. See arXiv:2607.14082.
Fig 1 (page 1).
Fig 1: An overview of the agentic formalization workflow and its trust boundary. The two rows follow artifacts
Fig 2: A dependency map of the Lean development used for the RSA-2048 and P-256 results. Solid arrows
Limitations
- The resource model is logical and idealized—real physical error correction, noise, and scheduling overheads are not modeled.
- Success probability bounds use assumptions of independent trials and simplified failure rates; deriving these rigorously within the formalization remains open.
- Classical recovery classical operation counts are at an abstract arithmetic step level, with no detailed cost modeling or hardware linkage.
- The formalization assumes idealized quantum hardware and does not incorporate fault-tolerance or noise-resilience results.
- The agentic formalization approach involves human review in interventions, so fully automated end-to-end formal proof generation is not yet achieved.
- Open challenges remain to integrate all individual resource and probability components into a single composite formal execution of the entire algorithm.
Open questions / follow-ons
- How to extend the formalization to model fault-tolerant quantum computing resource overheads including error correction and noise?
- Can the agentic formalization workflow be fully automated, reducing human review and intervention?
- How to integrate the separate formal proofs of quantum circuit behavior, probability bounds, and classical recovery into a single end-to-end machine-checked formal execution?
- Can this approach be extended to other quantum algorithms and cryptographic primitives beyond RSA and P-256?
Why it matters for bot defense
For bot-defense and CAPTCHA practitioners, this paper demonstrates a rigorous methodology to formally verify the concrete quantum resources and success probabilities underlying attacks on widely used cryptographic primitives like RSA-2048 and P-256. Understanding these formalized quantum costs informs security margins against future quantum adversaries. The detailed gate-level and success guarantees could guide assessments of when certain cryptographic schemes may become vulnerable and help design cryptographic parameters resilient to quantum attacks. While not directly related to CAPTCHA mechanisms, the formalized proofs and agentic proof engineering techniques could inspire rigorous security analyses and automated theorem-proving workflows in bot-detection or CAPTCHA verification protocols that involve cryptographic or complexity assumptions. The paper sets a standard for machine-checked quantum cryptanalysis, supporting trustworthy assessments of emerging attack vectors relevant to bot-defense infrastructure reliant on cryptographic hardness.
Cite
@article{arxiv2607_14082,
title={ Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256 },
author={ Lei Zhang and Yusheng Zhao and Hongshun Yao and Xin Wang },
journal={arXiv preprint arXiv:2607.14082},
year={ 2026 },
url={https://arxiv.org/abs/2607.14082}
}