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 coming up with this formula itself, is the probabilistic argument to show you always get the right answer.
So this seems simple enough to give a full Lean proof. And it is not too hard (for Claude) to get Lean to formalize the probabilistic argument, though even there Lean makes you deal with details we wave away on paper. When $x\not\in B$ the argument needs $n^k2^{-n}<1$, which fails for small $n$, so short inputs need separate handling. But you also need to show the following:
Let $A(x,r)$ be polynomial-time computable. Then given $x$, $y$ and the $z_i$ as inputs, you can compute $A(x,z_1\oplus y) \vee \cdots \vee A(x,z_{n^k}\oplus y)$ in polynomial time, where $u\oplus v$ is bitwise parity. There is nothing challenging about this statement. It is so painfully obviously true that I didn't even bring up this point in the 2025 post. But proving you can do this in polynomial time on a Turing machine, even though the only operations are bitwise parity, ORs and composition, is just very complicated to formalize in Lean.
Some suggest that using Cobham's characterization might be easier. But see below for what you need to do for bitwise parity alone. Imagine how complicated it would all get for something like Toda's theorem.
Update: Since I first drafted this post, OpenAI dropped a claimed Lean proof of L = RL = BPL, so maybe ignore this whole post?
Cobham defined his class as the smallest set of functions on the natural numbers (viewed as binary strings, with $|x|$ the length of $x$ and $|0|=0$) that contains the constant zero, the projections, the two successor functions $s_0(x)=2x$ and $s_1(x)=2x+1$, and the smash function $x#y=2^{|x|\cdot|y|}$, and that is closed under composition and bounded recursion on notation. The second operation defines a new function $f$ from functions $g$, $h_0$, $h_1$ in the class by $$
\begin{aligned}
f(0,\vec{y})&=g(\vec{y})\\
f(s_i(x),\vec{y})&=h_i(x,\vec{y},f(x,\vec{y}))
\end{aligned}
$$
for $i\in{0,1}$ and $s_i(x)\neq 0$, provided that $f(x,\vec{y})\leq k(x,\vec{y})$ for some $k$ already in the class. The recursion runs over the bits of $x$, so it takes only $|x|$ steps. The smash function gives the outputs polynomial growth in their lengths, and the bound $k$ keeps that growth from compounding over the recursion. Cobham's theorem says that this class is exactly the set of functions computable in polynomial time. As an example, consider bitwise XOR, $f(x,y)=x\oplus y$. The difficulty is that bounded recursion on notation peels bits off only one argument, while XOR has to move through $x$ and $y$ together. The fix is to recurse on a long enough counter $T$ and extract the bits of $x$ and $y$ by shifting. We first need four helper functions, each defined by a single bounded recursion on notation: $$ \begin{aligned} \mathrm{par}(0)=\mathrm{par}(s_0(x))&=0, & \mathrm{par}(s_1(x))&=1\ \mathrm{half}(0)&=0, & \mathrm{half}(s_i(x))&=x\ \mathrm{msp}(0,x)&=x, & \mathrm{msp}(s_i(w),x)&=\mathrm{half}(\mathrm{msp}(w,x))\ C(0,u,v)=C(s_0(a),u,v)&=u, & C(s_1(a),u,v)&=v \end{aligned} $$ with bounds $1$, $x$, $x$ and $s_1(u)#s_1(v)$ respectively. Here $\mathrm{msp}(w,x)=\lfloor x/2^{|w|}\rfloor$, so bit $j$ of $x$ is $\mathrm{par}(\mathrm{msp}(w,x))$ for any $w$ with $|w|=j$. $C$ is a conditional on the low bit of $a$. Composition then gives the XOR of the low bits of $a$ and $c$, $\beta(a,c)=C(a,\mathrm{par}(c),C(c,1,0))$, and appending the low bit of $b$ to $z$, $\mathrm{app}(b,z)=C(b,s_0(z),s_1(z))$.
Now we recurse on $w$ with $T$, $x$ and $y$ as parameters, building the answer from the top bit down. Let $m_i=\mathrm{msp}(s_i(w),T)$, which has length $|T|-|w|-1$, the position of the next bit to append, and let $b_i=\beta(\mathrm{msp}(m_i,x),\mathrm{msp}(m_i,y))$ be that bit of $x\oplus y$. Then $$ \begin{aligned} G(0,T,x,y)&=0\ G(s_i(w),T,x,y)&=\mathrm{app}(b_i,G(w,T,x,y)) \end{aligned} $$ By induction, $G(w,T,x,y)$ is $x\oplus y$ shifted right by $|T|-|w|$ bits, so it is bounded by $s_1(x)#s_1(y)$. Finally we set $$ f(x,y)=G(T,T,x,y)\quad\text{where } T=s_1(x)#s_1(y). $$ The smash gives $|T|=(|x|+1)(|y|+1)+1\geq\max(|x|,|y|)$, so the recursion starts above the high bits of both arguments, where every bit is zero. $T$ is much longer than it needs to be, but that costs only polynomially many extra steps.