View source for Derandomization of logarithmic space

'''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 ([https://github.com/openai/math 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''(log<sup>2</sup> ''n'') seed bits in this setting. Nisan's simultaneous simulation achieves polynomial time and ''O''(log<sup>2</sup> ''n'') space, Nisan and Zuckerman treated computations with few random bits, Saks and Zhou reduced the space to ''O''(log<sup>3/2</sup> ''n''), Cai, Chakaravarthy and van Melkebeek gave a time–space tradeoff, and Hoza improved the space bound by a factor of (log log ''n'')<sup>1/2</sup>.
** 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<sup>−''q''</sup> by a deterministic algorithm using ''O''(log(''n'' + 2) + ''q'') work space and (''n'' + 2)<sup>''O''(1)</sup>2<sup>''O''(''q'')</sup> 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026 Exact derandomization of logarithmic space: L = RL = BPL] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/103.md scope note], added to the repository on 8 October 2026 (commit <code>3014888</code>), 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 is <code>LogspaceEquality.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 || [https://github.com/raullenchai/ai-math-kills-crypto 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''(log<sup>2</sup> ''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: [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/LogspaceEquality.json run 38019899278] and [https://github.com/carlostoledo1891/cert-machine/blob/d2c6a255d759d4bcfa829ea72302d62d078886a6/corpus/openai-math/kernel-runs/38050007619/LogspaceEquality.json run 38050007619] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>LogspaceEquality</code> 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (tasks #348 and #353) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code> (task #348), Lean's official kernel accepted <code>LogspaceEquality</code>, 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 || [https://github.com/punk01-shaka/hadwiger-nelson-audit/issues/1 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 <code>definition_names</code>, so that Comparator checks only their names and types, and counts 20 such definitions in the <code>LogspaceEquality</code> configuration. With that configuration unmodified, it demonstrates that a fake solution making the three classes empty, with the proof <code>⟨rfl, rfl⟩</code>, 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 <code>definition_names</code>. || 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 #SAC<sup>1</sup> Functions in Logspace Uniform AC<sup>1</sup>'', [https://arxiv.org/abs/2610.25623v1 arXiv:2610.25623v1] || Remark (citation) || Shows that #SAC<sup>1</sup> functions can be approximated in logspace-uniform '''AC'''<sup>1</sup> with multiplicative error 2<sup>−poly log ''n''</sup>, 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) || [https://github.com/jiamo/lambda-computability/tree/035a085b376d957b0086455dbf8129c2a4b2f52f jiamo/lambda-computability] (GitHub, commit <code>035a085</code>) || Use (Lean port) || A Lean library on lambda calculus and computability that adapts the collection's <code>Logspace</code> formalization, taken from the collection's commit <code>3014888</code>, to its own Lean and Mathlib versions, with terminal theorems stating '''BPL''' ⊆ '''L''' and '''L''' = '''RL''' and '''RL''' = '''BPL'''. Its <code>NOTICE</code> 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 <code>NOTICE</code> 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.

[[Category:OpenAI results]]