True, but shortsighted. If we continue to pile proofs and new theorems on top of each other without taking care of making those new abstractions understandable, then we will limit our reach. Even though AI might be able to progress further.