On the other hand, programming languages are designed first to be easily parsed by computers. With supercomputers, exascale computing [0] is now possible. Yet it is still hard to use fully the power of such computers because what is intuitive for a human mind is not always easy to program. For example the video proof of the inversion of the sphere [1] is checked more easily by a human than by a computer.
Finally instead of using only the power of computers, or only the power of human brains, it is also possible to combine both. This requires to improve the interaction between computers and human beings. In a video on thinking the unthinkable [2], the author notably remarks that the introduction of symbols in algebra allowed human beings to extend the problems they could think about. With better interfaces, the computers could help us to write fuzzy or explicit proofs, but more importantly, they could help us to think.
[0]: https://en.wikipedia.org/wiki/Exascale_computing