# Exact quantum factoring over a fixed finite gate set

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Exact quantum factoring over a fixed finite gate set](../../preprints/Exact-quantum-factoring-over-a-fixed-finite-gate-set-September-25-2026/main.pdf)

## Scope

The formalization constructs a polynomial-time uniform quantum circuit family that outputs the complete prime factorization of every integer $N\ge2$ with probability exactly one. The circuits use one fixed finite set of bounded-arity gates, and both the gate count and number of qubits have polynomial worst-case bounds in the bit length of $N$. The probability-one conclusion is exact, rather than an asymptotic or bounded-error guarantee.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Exact quantum factoring over a fixed finite gate set | [ExactQuantumFactoring.lean](../ComparatorChallenges/ExactQuantumFactoring.lean) |