QudeLeapQuantumAlg

Lean-QuantumAlg

Lean v4.31.0 mathlib v4.31.0 CSLib v4.31.0 Apache License 2.0
QML paper on arXiv Shor paper on arXiv

Lean-QuantumAlg is a Lean 4 library for formally verified quantum algorithms.

What's Lean-QuantumAlg?

Lean-QuantumAlg provides reusable definitions, primitives, and theorem statements for quantum algorithms in Lean. It is built on mathlib and CSLib, with public theorem endpoints organized so readers and agents can import the modules they need.

Aims

  • Provide a modest, reusable Lean library for quantum-algorithm formalization.
  • Keep algorithm statements tied to source references and stable import paths.
  • Follow mathlib and CSLib conventions closely enough to support later upstream review and reuse.

Cite this repository

If you use the quantum machine learning or quantum neural network formalizations in Lean-QuantumAlg, please cite:

@misc{jing2026agentic,
      title={An Agentic Formalization for Certified Quantum Neural Network Design},
      author={Mingrui Jing and Lei Zhang and Yusheng Zhao and Hongshun Yao and Xin Wang},
      year={2026},
      eprint={2607.12981},
      archivePrefix={arXiv},
      primaryClass={quant-ph},
      url={https://arxiv.org/abs/2607.12981},
}

If you use Shor's algorithm, the RSA-2048 or P-256 developments, or broader quantum cryptanalysis formalizations in Lean-QuantumAlg, please cite:

@misc{zhang2026building,
      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},
      year={2026},
      eprint={2607.14082},
      archivePrefix={arXiv},
      primaryClass={quant-ph},
      url={https://arxiv.org/abs/2607.14082},
}

Using Lean-QuantumAlg in your project

To add Lean-QuantumAlg as a dependency to a Lake project, add the following to your lakefile.toml:

[[require]]
name = "QuantumAlg"
git = "https://github.com/QudeLeap/Lean-QuantumAlg.git"
rev = "main"

Use Lean v4.31.0. Then import either the aggregate module or a focused module:

import QuantumAlg
import QuantumAlg.Algorithms.Grover
import QuantumAlg.Algorithms.QPE
import QuantumAlg.Primitives.QFT

The library currently includes:

  • QuantumAlg.Core: pure states, gates, tensor products, measurement, and the shared CSLib TimeM cost adapter.
  • QuantumAlg.Core.Components: named gates, kets, oracle and control components.
  • QuantumAlg.Primitives: reusable quantum-algorithm primitives such as phase kickback, QSP, LCU, swap test, and amplitude amplification.
  • Circuit theorem endpoints: fixed-circuit statements such as Bell-state preparation, GHZ-state preparation, and QFT.
  • QuantumAlg.Algorithms: end-to-end algorithm/protocol statements including Deutsch-Jozsa, Bernstein-Vazirani, Grover, QPE, order finding, amplitude estimation, teleportation, superdense coding, and Simon.

Trusted cost annotations for query or iterate counts live beside the theorem endpoints they annotate and use the shared CSLib TimeM adapter.

For a quick build check:

lake exe cache get
lake build

For theorem discovery, start from QuantumAlg.lean or the module names above. Lean docstrings cite the source references using keys resolved by REFERENCES.json.

Quantum machine learning

Lean-QuantumAlg exposes two overlapping views of quantum machine learning: expressivity, and trainability with Lie-algebraic simulation.

Expressivity. Trigonometric polynomials and QSP/QSVT provide the polynomial transformation substrate, followed by parameter-shift rules, quantum kernels, and QFIM-based capacity bounds. Verified highlights include:

Trainability. The main results connect Lie-algebraic variance laws, explicit no-barren-plateau families, and exact loss reconstruction:

Start from the two focused public navigation modules:

import QuantumAlg.Primitives.QNN.Expressivity
import QuantumAlg.Primitives.QNN.Trainability

Bibliographic sources are indexed in REFERENCES.json.

Cryptanalysis

Lean-QuantumAlg formalizes source-backed endpoints for quantum cryptanalysis while keeping algorithmic correctness, conditional classical reductions, and logical-resource accounting explicit. The current results cover integer factoring and finite-cyclic discrete logarithms, together with formula-based estimates for RSA-2048 and P-256; each theorem states the certificates and hypotheses that connect a quantum routine to its cryptographic target.

Verified highlights include:

Start from the focused public navigation modules:

import QuantumAlg.Algorithms.Factoring
import QuantumAlg.Algorithms.FiniteCyclicDLP
import QuantumAlg.Algorithms.EllipticCurve

Contributing and discussion

Issues and pull requests are welcome. Please keep contributions small and source-backed: algorithm claims should cite public references, and Lean changes should build without sorry, admit, or new axioms.

License

Lean-QuantumAlg is released under the Apache License 2.0. See LICENSE.