Quantum Cryptography and Autoformalization in Lean

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.

Consecutive Measurement Tradeoffs in Quantum Cryptography
Chen-Xun Weng, Minglong Qin, Yanglin Hu +1
PRX Quantum15 Oct 2026Peer-reviewedPublisher termsQuantum physics & quantum informationCrossref
From Quantum Cryptography to Intuitionism and beyond: relativity, many-worlds and non-locality
Nicolas Gisin
arXiv7 Sep 2026PreprintCC BY 4.0Full textQuantum physics & quantum informationarXiv
Reliable Entropy Estimation from Observed Statistics for Device-Independent Quantum Cryptography
Gereon Koßmann, René Schwonnek
Quantum20 Oct 2026Peer-reviewedCC BY 4.0Full textQuantum physics & quantum informationCrossref
Need for Coherent Access in Constructing Quantum Cryptography
Minki Hhan, Changhun Oh, Vaughn Sohn
arXiv30 Sep 2026PreprintarXiv licenceFull textQuantum physics & quantum informationarXiv
quantum-safe: Bridging the Post-Quantum Production Gap with a Hybrid-by-Default Python Cryptography Library
Animesh Shaw
arXiv6 Oct 2026PreprintCC BY 4.0Full textQuantum physics & quantum informationarXiv

Cite

BibTeX RIS

BibTeX

@misc{shahar2026quantum,
  title = {{Quantum Cryptography and Autoformalization in Lean}},
  author = {Maor Ben Shahar and Jonathan Morag and Dirk Englund and Kfir Sulimany},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.17286},
  eprint = {2610.17286},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.17286},
  note = {CC BY 4.0},
}

RIS

TY  - UNPB
TI  - Quantum Cryptography and Autoformalization in Lean
AU  - Maor Ben Shahar
AU  - Jonathan Morag
AU  - Dirk Englund
AU  - Kfir Sulimany
PY  - 2026
DA  - 2026/10/12
PB  - arXiv
DO  - 10.48550/arxiv.2610.17286
UR  - https://arxiv.org/abs/2610.17286
AB  - 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.
ER  -

Abstract

Related

Cite