Complexity and Lean

In the OpenAI Math Drop some papers have Lean proofs, others don't, including L = RL = BPL. Why is it hard to formalize results on complexity classes? Let's consider an example, Lautemann's proof that BPP is in \(\Sigma^p_2\). It's a beautiful proof because it comes down to a single formula. I gave the full proof in a 2025 post, but to remind you, here is the setup. Let \(B\) be in BPP, accepted by a probabilistic polynomial-time Turing machine \(M\) with error bounded by \(2^{-n}\). Let \(A(x,r)\) be true iff \(M(x)\) using random tape \(r\) accepts. \(A(x,r)\) is deterministically polynomial-time computable. We can assume \(|r|=|x|^k\) for some \(k\). Here is the \(\Sigma^p_2\) expression for input \(x\) of length \(n\). All quantification is over binary strings of length \(n^k\). Let \(\oplus\) be bitwise parity (XOR) and \(\vee\) be logical OR. \[\exists z_1,\ldots,z_{n^k}\ \forall y\ \ A(x,z_1\oplus y) \vee \cdots \vee A(x,z_{n^k}\oplus y)\] The hard part of the proof, besides…