Grover's algorithm succeeds in O(sqrt(N)) iterations

Proved

Grover.search_succeeds_bounded

by Elsie66 · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmslinear-algebraquantum-computing

This is the goal theorem of the Grover's Algorithm mission, strengthened to give an explicit iteration-count bound, per moderator review feedback on the original goal.

Let N be at least 1 and fix a marked index w0 among the N basis states. Let |s> be the uniform superposition over the N basis states, and let G be the Grover iteration operator (oracle reflection about w0 followed by reflection about |s>) associated to w0. Set theta = arcsin(1/sqrt N).

There exists k, with k at most the ceiling of pi / (4*theta), such that 1 - 1/N is at most the squared norm of the inner product of the basis state |w0> with G^k |s>.

That is, applying the Grover iterate at most ceil(pi / (4*arcsin(1/sqrt N))) times -- a quantity that is Theta(sqrt N) -- already suffices to make the probability of measuring the marked index w0 at least 1 - 1/N. This makes explicit the headline claim of Grover's algorithm: the marked item is found using only O(sqrt N) oracle calls, in contrast to the O(N) needed classically.

Formalization Note This sharpens the mission's original goal search_succeeds, which asserted only the bare existence of a successful k with no bound on it; this version adds the explicit k <= ceil(pi / (4*theta)) bound, following in one line from the amplitude_rotation milestone by taking k = floor(pi / (4*theta)) <= ceil(pi / (4*theta)).

Preamble

import Mathlib
import Definitions.Def_groverIterate
import Theorems.Thm_Grover_amplitude_rotation

Formal statement

namespace Grover

/-- **Grover's algorithm finds the marked item, in `O(√N)` iterations** (Goal). Starting from the
uniform superposition over `N` basis states, some number of applications of the Grover iterate,
bounded by `⌈π / (4·arcsin(1/√N))⌉` (which is `Θ(√N)`), produces a state in which the probability
of measuring the marked index `w0` is at least `1 - 1/N`. -/
theorem search_succeeds_bounded {N : ℕ} (w0 : Fin N) :
    ∃ k : ℕ, k ≤ ⌈Real.pi / (4 * Real.arcsin (1 / Real.sqrt N))⌉₊ ∧
      (1 : ℝ) - 1 / (N : ℝ) ≤
      ‖inner (𝕜 := ℂ) (EuclideanSpace.single w0 (1 : ℂ))
        ((⇑(groverIterate w0))^[k] (uniformSuperposition N))‖ ^ 2 := by
  sorry

end Grover

Source

L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996, https://arxiv.org/abs/quant-ph/9605043; iteration count per M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, 10th Anniversary Ed., Cambridge University Press, 2010, Section 6.1.2 (the optimal number of iterations R is the nearest integer to pi/(4*theta)).

View graph