Comment by returningfory2

A tiny fraction compared to the proof, I'm guessing.

But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.