Kothari: quantum exact learning with O(√((1/γ)/log(1/γ))·log|C|) queries

Open

QAlgorithms.LearningSurvey.kothari_quantum_exact_upper

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

learning-surveylecture-notesquantum-information

This is Kothari's upper bound on quantum exact learning in terms of the combinatorial parameter $\gamma(C)$ .

Let $N=2^n$ and let $C\subseteq\{0,1\}^N$ be a concept class with $|C|\ge 2$ , and let $\gamma(C)$ be as in Definition 4.1. There is an absolute constant $K>0$ such that for every such $C$ there is a quantum exact learner for $C$ (input-independent unitaries interleaved with $T$ queries to $O_c:|x,b\rangle\mapsto|x,b\oplus c(x)\rangle$ , outputting $h=c$ with probability at least $2/3$ for every target $c\in C$ ) with

T\ \le\ K\sqrt{\frac{1/\gamma(C)}{\log(1/\gamma(C))}}\ \log|C| .

It nearly matches the $\Omega(1/\sqrt{\gamma(C)})$ lower bound of Theorem 4.3 and resolved a conjecture of Hunziker et al.

Formalization Note Since $|C|\ge 2$ forces $0<\gamma(C)\le 1/2$ , the logarithm $\log(1/\gamma(C))\ge\log 2$ is positive. The logarithm is natural; the base only changes $K$ .

Preamble

import Definitions.Def_QAlgorithms_Defs_LearningHardInstances
set_option autoImplicit false

Formal statement

namespace QAlgorithms.LearningSurvey

universe u





/-- **Theorem 4.8** (Kothari; survey p.12). For every concept class `C ⊆ {0,1}^N` (`N = 2^n`,
`|C| ≥ 2`, the domain of `γ`), there is a quantum exact learner for `C` using
`O(√((1/γ(C)) / log(1/γ(C))) · log |C|)` quantum membership queries. The constant `K` is absolute;
the learner is chosen after `C` but before the target concept. -/
theorem kothari_quantum_exact_upper :
    ∃ K : ℝ, 0 < K ∧ ∀ (n : ℕ) (C : Finset (Qubits n → Bool)), 2 ≤ C.card →
      ∃ (w T : ℕ) (A : QueryAlg (Qubits n) Bool (Fin w) T)
        (out : (Qubits n × Bool) × Fin w → (Qubits n → Bool)),
        Learning.IsQExactLearner A out C ∧
          (T : ℝ) ≤ K * Real.sqrt ((1 / Learning.gammaParam C) /
            Real.log (1 / Learning.gammaParam C)) * Real.log (C.card : ℝ) := by
  sorry

end QAlgorithms.LearningSurvey

Source

Srinivasan Arunachalam and Ronald de Wolf, A Survey of Quantum Learning Theory, 2017, v3, PDF p. 12, §4.1.2, Theorem 4.8. https://arxiv.org/pdf/1701.06806v3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Concepts, $T$ -query quantum algorithms $U_T(O\otimes I)\cdots(O\otimes I)U_0|s\rangle$ with XOR oracle $O_c:|x,b\rangle\mapsto|x,b\oplus c(x)\rangle$ , output maps, and exact learning (for every $c\in C$ , the computational-basis measurement yields a label mapped to $c$ with probability $\ge 2/3$ ) are as in the first entry. So is the parameter

\gamma(C)=\min_{C'\subseteq C,\ |C'|\ge 2}\ \max_{i}\ \min\bigl(\gamma_{C'}(i,0),\gamma_{C'}(i,1)\bigr),

where $\gamma_{C'}(i,b)$ is the fraction of $c\in C'$ with $c(i)=b$ .

Statement. There is a constant $K>0$ such that for every $n\in\mathbb N$ (including $n=0$ ) and every concept class $C$ on $\{0,1\}^n$ with $|C|\ge 2$ , there exist:

a workspace size $w\in\mathbb N$ and a query count $T\in\mathbb N$ ;
a $T$ -query algorithm $A$ with workspace $\{0,\dots,w-1\}$ ;
an output map $\mathrm{out}$ ,

such that $(A,\mathrm{out})$ exactly learns $C$ and

T\ \le\ K\sqrt{\frac{1/\gamma(C)}{\ln\bigl(1/\gamma(C)\bigr)}}\ \ln|C| .

Here $\ln$ is the natural logarithm, and divisions by zero, if any arose, would evaluate to $0$ .

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph