Pure Maths in Crisis?

Such software won’t magically find proofs of difficult results that have eluded people for centuries — human mathematicians are still very much needed — but it can help you check your proofs are sound. This means that many monumental results in maths, including Fermat’s last theorem or the classification of finite simple groups, to a computer scientist’s mind could still be checked more carefully. Buzzard is aware that turning their proofs into the code the software can understand would involve a phenomenal effort — for Fermat’s last theorem, Buzzard estimates it would cost around a 100 million pounds — but he is suggesting that at least we could teach budding mathematicians to embrace the approach.

Source: plus.maths.org