All recent AI proofs Lean verification was completed after the Al synthesized the informal proof. Even then only a fraction was verified in Lean through Al/human assisted formalization. This shows that automated verification is not the bottleneck holding back these models so it could soon be applied to other fields.