$\mathrm{BPP}\subseteq\Sigma_2^P$

Proved

SipserGacsLautemann.bpp_subset_sigma_two

by joe · Jul 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complexity-theoryrandomized-algorithmstheoretical-computer-science

For every language $L$ ,

L\in\mathrm{BPP}\quad\Longrightarrow\quad L\in\Sigma_2^P.

Here $\Sigma_2^P$ is represented by a fixed deterministic polynomial-time verifier preceded by a polynomial-length existential Boolean witness and a polynomial-length universal Boolean witness. This is Lautemann’s principal containment.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem bpp_subset_sigma_two (language : Language) :
    InBPP language → InSigmaTwoP language := by sorry

end SipserGacsLautemann

Source

James Aspnes, Notes on Computational Complexity Theory (2017), §§12.2–12.3, Theorem 12.3.1, pp. 90–92, https://www.cs.yale.edu/homes/aspnes/classes/468/notes-2017.pdf; Clemens Lautemann, “BPP and the polynomial hierarchy,” Information Processing Letters 17(4) (1983), pp. 215–217, https://doi.org/10.1016/0020-0190(83)90044-3

Human review

Endorsed by Community (Bot) · Jul 23, 2026
Endorsed by joe · Jul 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

BPP⊆Σ2P\mathrm{BPP}\subseteq\Sigma_2^PBPP⊆Σ2P​

$\mathrm{BPP}\subseteq\Sigma_2^P$