Derandomization of logarithmic space
From OpenAI Aftermath
Derandomization of logarithmic space concerns whether randomized algorithms that use logarithmic memory and polynomial time can be simulated by deterministic algorithms with logarithmic memory, that is, whether the complexity classes L, RL and BPL coincide. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims L = RL = BPL, together with a deterministic logarithmic-space approximation of acceptance probabilities and an effective compiler. The collection includes a Lean formalization of the class equality. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Gill developed the complexity theory of probabilistic Turing machines. Aleliunas, Karp, Lipton, Lovász and Rackoff gave a randomized logarithmic-space algorithm for undirected connectivity and asked whether polynomial-time randomized logarithmic space can be simulated in deterministic logarithmic space; Borodin, Cook and Pippenger gave a quadratic-space deterministic simulation without the polynomial-time restriction.
- Pseudorandom generators replace long random strings by short seeds: Ajtai, Komlós and Szemerédi, and Babai, Nisan and Szegedy gave early constructions, and Nisan's generator uses O(log2 n) seed bits in this setting. Nisan's simultaneous simulation achieves polynomial time and O(log2 n) space, Nisan and Zuckerman treated computations with few random bits, Saks and Zhou reduced the space to O(log3/2 n), Cai, Chakaravarthy and van Melkebeek gave a time–space tradeoff, and Hoza improved the space bound by a factor of (log log n)1/2.
- For undirected connectivity, Nisan, Szemerédi and Wigderson, and Armoni, Ta-Shma, Wigderson and Zhou, reduced the space, and Reingold's algorithm settled the problem in logarithmic space; Reingold, Trevisan and Vadhan treated Eulerian directed graphs. Cheng and Hoza showed that suitable hitting sets for read-once branching programs would give L = BPL. The manuscript also cites recent work of Chen, Cohen, Doron, Khaskelberg and Ta-Shma, of Cheng and Wu, of Pyne and Tell, and the universal estimator of Pyne, Raz and Zhan.
The original result
- Claim. Theorem 1.1 of Exact derandomization of logarithmic space: L = RL = BPL states L = RL = BPL, where RL and BPL consist of languages decided by polynomial-time randomized machines in logarithmic work space with one-sided error (acceptance probability 0 on no-instances, at least 1/2 on yes-instances) and two-sided error (at most 1/3 and at least 2/3). Theorem 1.2 states that the acceptance probability of such a machine can be approximated to within 2−q by a deterministic algorithm using O(log(n + 2) + q) work space and (n + 2)O(1)2O(q) time. Theorem 13.1 gives a terminating compiler which, given a source program and supplied time and space bounds, produces a deterministic decider with explicit numerical space and time bounds.
- Method, as described: the computation is reduced to a strictly forward substochastic matrix on configurations, whose resolvent records acceptance probabilities; a hierarchy of copies of configurations with accumulated rewards approximates the acceptance probability of the start configuration; the resulting quantity is estimated in a shared random environment described by O(log n) bits, with a moment bound showing that more than three quarters of the environments give accurate estimates, and every environment is evaluated by a halting deterministic logarithmic-space computation, so that exhaustive enumeration gives the deterministic answer.
- Sources. The manuscript Exact derandomization of logarithmic space: L = RL = BPL at commit
1581d4c. - Formalization, as described by the repository. The scope note, added to the repository on 8 October 2026 (commit
3014888), states that the formalization proves L = RL = BPL for binary languages in an explicit Turing-machine model with logarithmic workspace, with the randomized classes in polynomial time, and that the paper's explicit compiler and numerical running-time bounds are not separately stated in the Comparator target. The Comparator statement isLogspaceEquality.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the Lean statement gives L = RL and RL = BPL for binary languages in an explicit multi-tape logarithmic-space Turing-machine model with one fresh coin per step and a polynomial clock on every coin tape, which it describes as the paper's main theorem after unfolding the definitions, the binary alphabet being a routine convention. It notes that the effective compiler with explicit running-time bounds has no Lean statement, as the scope note says, and records a sandboxed Comparator pass for the challenge. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-08 | raullenchai/ai-math-kills-crypto (GitHub) | Remark | A survey of the cryptographic consequences of selected OpenAI results. It states that, among polynomial-time deterministic simulations, the workspace bound improves from O(log2 n) to O(log n), but that the theorem needs a randomized logarithmic-space program for the target problem as its input, so that no new key-recovery cost estimate follows. | GitHub page. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 and run 38050007619 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the LogspaceEquality solution, in 476 s and again in 517 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (tasks #348 and #353) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb (task #348), Lean's official kernel accepted LogspaceEquality, while con-leche stopped with exit code 3 because its reduction fuel was exhausted on a deep recursion. After the changes of task #353, the journal records that con-leche accepts the challenge (3.7 GB). |
Development journal. |
| 2026-10-12 | Issue #1 in the GitHub repository punk01-shaka/hadwiger-nelson-audit | Critique (formalization setup) | The issue states that several of OpenAI's Comparator configurations declare fully written definitions as definition_names, so that Comparator checks only their names and types, and counts 20 such definitions in the LogspaceEquality configuration. With that configuration unmodified, it demonstrates that a fake solution making the three classes empty, with the proof ⟨rfl, rfl⟩, is accepted by Comparator. It states that this does not show any result to be wrong, only that the check as configured does not certify the result on its own, and suggests removing such definitions from definition_names. |
Open issue. The fake solution is labelled as such in the repository; it is not the solution published in the collection. |
| 2026-10-19 | K. Cheng, S. Huang, R. Wu, High Precision Multiplicative-Error Approximation of #SAC1 Functions in Logspace Uniform AC1, arXiv:2610.25623v1 | Remark (citation) | Shows that #SAC1 functions can be approximated in logspace-uniform AC1 with multiplicative error 2−poly log n, with corollaries for randomized logarithmic-space machines with an auxiliary pushdown store and for read-k randomized logarithmic space. The abstract notes "that recently OpenAI announced that BPL = L" and states that, even for derandomizing BPL, its computation has the advantage of a multiplicative error of that size. | arXiv preprint, version 1 of 19 October 2026. |
| 2026-10-20 (latest commit) | jiamo/lambda-computability (GitHub, commit 035a085) |
Use (Lean port) | A Lean library on lambda calculus and computability that adapts the collection's Logspace formalization, taken from the collection's commit 3014888, to its own Lean and Mathlib versions, with terminal theorems stating BPL ⊆ L and L = RL and RL = BPL. Its NOTICE file states that "the mathematics and the proofs are upstream's" and records the renamings and one changed proof step. |
GitHub repository (created before the release; the adaptation is listed in its NOTICE file).
|
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
