Comment by skobes

Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?

How have we not merely substituted one verification problem for another?