Shannon was 1948, one-way crypto in 1978, univalence/HoTT something like 2007; I would be surprised if there weren’t simple new fundamental primitives out there! One problem is that some great advances are from viewing complex objects in a simple way, which take a lot of characters to define in formal logic but which are “simple” in platonic maths-space.

1. The computer is going to struggle to recognize elegance. I’m not sure it’s relevant at this point (but who knows).

2. The statement about proofs is just way wrong. It doesn’t sound like you are familiar enough with them.

This isn’t exactly what you implied, but witness the very short disproof of the Jacobean Conjecture.