Comment by amelius

> It sounds horrible to wade through - like trying to understand someone else's messy code that still produces the correct output.

Makes you wonder if AI can build upon such proofs.

If the AI cannot create proper abstractions, then how can it build a tower of abstractions?