oai-math-revised beta

Browse › Theoretical computer science › 103 Exact derandomization of logarithmic space: $\mathsf L=\mathsf{RL}=\mathsf{BPL}$

Exact derandomization of logarithmic space: L = RL = BPL

OpenAI · September 23, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

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

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

Comments and discussion

  • Ran Raz, quoted in Peter Hall and Joseph Howlett, The most exciting claims from OpenAI's heap of new proofs (Scientific American, 8 October 2026). The article includes Problem 103 among highlighted claims, explains $\mathsf L=\mathsf{RL}$ for a general audience, and quotes Raz on its status before this paper ("I didn't see any directions that were promising [before]"); it does not report any assessment of the proof itself.
  • Scott Aaronson, The Mathocalypse (Shtetl-Optimized, 7 October 2026). Lists L = BPL among the results he expects to follow most closely, calling it "one of the great derandomization conjectures short of P=BPP", and reproduces, with permission, Omer Reingold's reaction specifically to RL versus L.

Formalization

  • OpenAI math release, Lean scope notes for family 103 (release file lean/docs/103.md). Says the Lean target asserts $\mathsf L=\mathsf{RL}=\mathsf{BPL}$ for binary languages in an explicit Turing-machine model with logarithmic workspace. The paper's explicit compiler and numerical running-time bounds are not separately stated.
  • OpenAI, LogspaceEquality.lean (Comparator challenge statement) (openai/math, October 2026). Defines finite transition-table machines with a coin bit and states exact_logarithmic_space_derandomization : L = RL ∧ RL = BPL, with theorem body sorry. Its L definition has no explicit polynomial clock; RL/BPL use a fixed polynomial clock.
  • Lance Fortnow, Complexity and Lean (Computational Complexity blog, 15 October 2026). Discusses why complexity results are hard to formalize. An update notes that OpenAI "dropped a claimed Lean proof of L = RL = BPL".

Possibly relevant literature (found by the agent, not checked)

Digests and expositions

News and blogs

  • Lance Fortnow, Open No More (Computational Complexity blog, 7 October 2026). Lists "a full derandomization of randomized log space" among the release's results, with the caveat that the proofs "haven't been fully verified". Several anonymous commenters express doubt about this result.
  • Azmat, Derandomization of Logarithmic Space: Inside OpenAI's Bold L = RL = BPL Breakthrough Claim (Binary Verse AI, 8 October 2026). A popular article summarizing the acceptance-probability approximation, the correction-and-copy hierarchy, the median over enumerated estimators and workspace requirements, distinguishing the asymptotic claim from practical speedups. It notes that the result has not been independently verified.

Elsewhere

Independent sites; their content is not reviewed here.

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}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/103.md. The Lean statements have not been checked by people against the paper's claims.

Family 103: 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.

This is the only paper in this family.