> onsider Fermat's conjecture. It's trivial to state it, it's trivial to test it to be correct for a given set of inputs. However, proving it for the general case is quite difficult, and only a handful of people in the world can follow that proof.

This is a strawman, conventional static type system can't prove all general cases either and no body is saying that they do that. Yet, they being a superset of dynamic typing, they allow to have the same expesiveness as such by providing a bypass like 'Object' or 'any'.