Theoretical computer science · Result 103

Exact derandomization of logarithmic space: \(\mathsf L=\mathsf{RL}=\mathsf{BPL}\)

1 paperLean

Proves \(\mathsf L=\mathsf{RL}=\mathsf{BPL}\), resolving derandomization for bounded-error logarithmic-space computation. An effective compiler converts each randomized polynomial-time logarithmic-space machine deciding a language with one-sided or two-sided error into a deterministic logarithmic-space decider with explicit polynomial running-time bounds.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Exact derandomization of logarithmic space: L = RL = BPL

OpenAI · September 23, 2026

We prove \(\mathsf L=\mathsf{RL}=\mathsf{BPL}\), resolving the derandomization problem for polynomial-time randomized logarithmic space.

Read PDF Download Source

Cite

@misc{OAI:Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026,
  author = {{OpenAI}},
  title = {{Exact Derandomization of Logarithmic Space:
            $\mathsf{L}=\mathsf{RL}=\mathsf{BPL}$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/paper.pdf}{OAI:Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

Exact derandomization of logarithmic space: L = RL = BPL

Scope

The formalization proves \(\mathsf L=\mathsf{RL}=\mathsf{BPL}\) for binary languages in an explicit Turing-machine model with logarithmic workspace. The randomized classes use polynomial time: \(\mathsf{RL}\) never accepts a no-instance and accepts a yes-instance with probability at least \(1/2\), while \(\mathsf{BPL}\) has acceptance probability at least \(2/3\) on yes-instances and at most \(1/3\) on no-instances. Thus bounded-error randomness does not enlarge deterministic logarithmic space in this model.

The selected theorem asserts equality of the language classes. The paper's explicit compiler and numerical running-time bounds are not separately stated in this Comparator target.

Comparator links

Result	Comparator statement
Exact equality of deterministic and randomized logarithmic space	LogspaceEquality.lean

Scope note on GitHub →