OpenAI claims L = RL = BPL with a Lean proof

Your AI and this story

Key facts

• Theorem 1.1 (verbatim): ‘L = RL = BPL.’ Theorem 1.2: for a polynomial-time O(log n)-space randomized machine, a deterministic algorithm on input (x, 1^q) approximates the acceptance probability within 2^−q using O(log(n + 2) + q) work space and (n + 2)^{O(1)} 2^{O(q)} time. About 358k characters, with 13 sections ending in ‘The effective compiler’
• Model (paper): finite control, endmarked read-only input, finitely many work tapes, fresh fair bits; ‘Space counts traversed writable cells in bits, including every simultaneously live counter, numerical register and suspended call’. RL: acceptance probability 0 on no-inputs and ≥ 1/2 on yes-inputs; BPL: ≤ 1/3 and ≥ 2/3; polynomial running time on every random tape
• Prior state (as recounted in the paper): Nisan’s generator, the Nisan–Zuckerman simulation, Saks–Zhou’s O(log^{3/2} n) deterministic space for general bounded-error logspace (JCSS 1999), and Hoza’s slight improvement of that bound (APPROX/RANDOM 2021). Full derandomization (BPL = L) remained open
• Lean: added to openai/math in the 7 Oct update (commit dated 8 Oct, 05:03 UTC). The scope note says the target 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 run (oai-math-revised, 26 Oct): LogspaceEquality ‘accepted’, with the caveat that the configuration listed 20 definitions ‘whose bodies the comparator does not compare, only their types’. OpenAI’s 26 Oct update emptied that list, so later runs compare the bodies too
• Re-check (ZHAO Han, @Beltran12138, oai-math-recheck family 103; recorded 28 Oct, prepared with Claude Code): the 55 OAI constants reachable from the statement, bodies included, dump byte-identical from the challenge and from OpenAI’s solution, on arm64 and x86_64. A negative control that changes only the body of BPL (error 1/3 → 1/2) is rejected. 39/39 modules build against Mathlib d13f23b. ‘Not shown: that the machine model is the standard one for L, RL and BPL. The re-check gives a reading of the definitions, not a proof of that.’
• Reactions: none found from complexity theorists as of 29 Oct (web, HN). An HN commenter (7 Oct) recalled ‘rumblings’ two weeks earlier that ‘RL=L’ and other results ‘were about to be proven’. The 6–7 Oct viral list of claims ranked ‘BPL = L’ #161 among ‘500 most important open problems’ (an LLM-ranked list)