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

Puntos clave

• ▸Covers the full stack in Lean: order finding, and reversible circuits for modular and elliptic-curve arithmetic.
• ▸Machine-checks the logical resource estimates for attacking RSA-2048 and the NIST P-256 elliptic curve.
• ▸Uses agentic formalization — AI agents draft and repair Lean proofs, with humans reviewing the scientific claims.

En lenguaje sencillo

Everyone planning for post-quantum cryptography relies on estimates of how big a quantum computer would need to be to break RSA-2048. Those figures decide migration budgets and deadlines — but they come from long, intricate papers that few people can fully verify by hand. This team rebuilt the argument inside Lean, a proof assistant that mechanically checks every step, so the estimates are backed by proofs a computer has validated rather than by trust in the authors. The twist is how they did it: AI agents wrote and repaired much of the formal proof, with humans checking the scientific claims. It is a useful signal in two directions at once — for how seriously to take RSA-breaking timelines, and for how far AI has come as a partner in formal mathematics.

Por qué importa

Post-quantum migration timelines rest on resource estimates: how many qubits and operations breaking RSA would actually take. Those numbers have historically come from hand-written analyses that are hard to audit. Putting them on a machine-checked footing makes the security planning that depends on them far more trustworthy.