The scary complex field of Math worried the mathematicians who would prove a theorem relying on the previous theorems assumed proven correct by other mathematicians.
A sad example was Zhang YiTang (1955 – ) who prepared his PhD Thesis based on a previous “flawed” Theorem proved by none other than his PhD Advisor Prof Mok in Purdue University. Unfortunately his Thesis was found wrong, and the tragic happened to Zhang as he had revealed the mistake of his PhD advisor who insisted his (Mok’s) Theorem was correct. As a result Zhang failed the 7-year PhD course without any teaching job recommendation letter from his angry advisor. He ended with a Subway Sandwich Kitchen job offered by his Chinese friend, sleeping in another Chinese music conductor’s house on a sofa. It was there he spent another 7 years thinking on Math, finally an Eureka breakthrough one 2013 morning in the backyard wild forest – the proof of the famous “70 million Prime Gap Conjecture”!
Univalent Foundation was born out of the same requirement by the (late) mathematician Vladimir Voevodsky (1966 – 2017) [#] – Use computer to prove Mathematics !
Note : [#] Vladimir Voevodsky