Quantum Cryptography and Autoformalization in Lean
Maor Ben Shahar, Jonathan Morag, Dirk Englund, Kfir Sulimany
quant-ph
Oct 12, 2026 · v1
TL;DR
End-to-end composable finite-key security of entanglement-based BB84 formalized in Lean 4 with Mathlib, developed via LLM-agent autoformalization; library released open source.
Abstract
Quantum key distribution provides secure communication by relying on physics principles and mathematical reasoning. Security proofs across the field can contain gaps, often between individually valid theorems integrated under mismatched assumptions. We produce an end-to-end security theorem formalized in the Lean proof assistant, eliminating hidden hypotheses by building only on Lean's standard axioms. Our proof covers composable security of the entanglement-based qubit BB84 protocol against coherent attacks by the postselection technique, accounting for finite block size, and is written in a language that enforces local operations and classical communication to help ensure a faithful representation of the protocol. The proof itself was enabled by LLM-based autoformalization, and with the proof complete, we used the same pipeline as a discovery machine, reducing the finite-size penalty on the key rate. Our work sets a reproducible standard for security arguments in quantum cryptography and shows how formal proof engines can accelerate discovery across quantum information science.
Problem
Security proofs for quantum key distribution can contain gaps caused by combining individually valid theorems under mismatched assumptions. No prior formal verification gave an end-to-end composable finite-key security bound for BB84 against general attacks.
Approach
Researchers worked iteratively with LLM agents based on Claude, GPT and a local GLM model. The agents translated statements from the literature into Lean 4 on top of Mathlib, guided by compiler feedback and dependency-graph tooling. A Lean language for LOCC programs enforces locality and makes public communication explicit by construction. The entanglement-based qubit BB84 protocol is defined in this language, and its composable security against coherent attacks is proved using the postselection technique with finite block size.
Results
The machine-checked security theorem depends only on Lean's standard axioms. The pipeline also found and proved a new conditional-entropy variance bound, log2²(√d + √(d−1)), which lowers the binary-key constant from about 5.39 to about 1.62 and reduces the finite-size key-rate penalty. The formalization exposed implicit assumptions in prior literature, and the quantum-information library is released open source.
