Computers need proofs by humans (Score 1)

Humans have been creating more and more proofs for the benefit of computers. They're just not recognized as such because these efforts are independent of mainstream mathematics.

It's called computer programming. The Curry-Howard correspondence demonstrates that every program in a statically typed language represents a proof, with the same kind of formality as the mathematical proofs mentioned in the article.