Reading the story[1] about Voevodsky, I was reminded of how Bertrand Russell described Gottlob Frege as "almost superhuman":
> As I think about acts of integrity and grace, I realise that there is nothing in my knowledge to compare with Frege’s dedication to truth. His entire life’s work was on the verge of completion, much of his work had been ignored to the benefit of men infinitely less capable, his second volume was about to be published, and upon finding that his fundamental assumption was in error, he responded with intellectual pleasure clearly submerging any feelings of personal disappointment. It was almost superhuman and a telling indication of that of which men are capable if their dedication is to creative work and knowledge instead of cruder efforts to dominate and be known. [2]
And how rare it is to see such "exceptionally honest" academic dialogue as Frege's:
> Frege starts his analysis by this exceptionally honest comment : "Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr Bertrand Russell, just when the printing of this volume was nearing its completion" [3]
Voevodsky too, upon finding himself in the same position as Frege, reacted with a super-human level of integrity and intellectual honesty:
> In 1998, the American mathematician Carlos Simpson published a paper indicating there might be a mistake in Voevodsky and Kapranov’s 1990 result. For years Voevodsky sifted through the details without making much progress. He remained convinced the result was right. Then, in the autumn of 2013, as the leaves changed color and summer gave way to autumn, he made a breakthrough. Of sorts. He confirmed the error. The important result was no longer quite so important.
> “It is plainly wrong. The main theorem is incorrect,” he says. “It’s not that there is some gap in the proof. It’s that the main theorem is plainly wrong.” The mistake, he explains, was in failing to question the obvious. “We had proved that an assertion was indeed true in all of the difficult cases, but it turned out to be false in the simple case. We never bothered to check.” In confirming the error, he added an addendum to the original citation in his official publications list—“Warning: The main theorem of this paper was shown by Carlos Simpson to be false.” [1]
It is all the more remarkable that he spent years of working through painstaking details to prove to himself that he was wrong. And rather than quietly issuing a retraction, he shouted it from the rooftops, leading a heroic charge to get mathematicians to stop hand-waving with English-language proofs, and start writing code. [4]
> And I now do my mathematics with a proof assistant. I have a lot of wishes in
terms of getting this proof assistant to work better, but at least I don’t have to go
home and worry about having made a mistake in my work. I know that if I did
something, I did it, and I don’t have to come back to it nor do I have to worry
about my arguments being too complicated or about how to convince others that
my arguments are correct. I can just trust the computer. There are many people in
computer science who are contributing to our program, but most mathematicians
still don’t believe that it is a good idea. And I think that is very wrong.[5]
1. https://nautil.us/issue/24/error/in-mathematics-mistakes-are...
2. https://plato.stanford.edu/entries/russell-paradox/
3. https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-...
4. https://www.quantamagazine.org/univalent-foundations-redefin...
5. https://www.ias.edu/sites/default/files/pdfs/publications/le...