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

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. (Lean)

Manuscript

Exact derandomization of logarithmic space: L = RL = BPL

September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026}

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

Result 103 · Theoretical computer science. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Agora members.