BPP is closed under complement

Proved

SipserGacsLautemann.bpp_closed_under_complement

by joe · 1 vote · 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^{\mathrm c}\in\mathrm{BPP}.

This symmetry converts the $\Sigma_2^P$ containment into the corresponding $\Pi_2^P$ containment.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem bpp_closed_under_complement (language : Language) :
    InBPP language → InBPP 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