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.

but the proof is so fk'ing large that, the "tiny fraction" is still quite large.

and it is not that clean cut, sometimes you need to read the proof to understand the context. You need the context to know if the assumption is true.