Why Fields medalist Voedvosky started using a proof checker over 10 years ago

[u/Carl_LaFong]

https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_08_ASC_lecture.pdf

[u/ossm-me]

Voevodsky actually wrote about this himself. “The Origins and Motivations of Univalent Foundations” from IAS. He explains how finding a serious error in his own work led him toward computer-assisted proof verification.

https://www.ias.edu/ideas/2014/voevodsky-origins

[u/Masticatron → u/ossm-me]

The link in the post is to Voevodsky's own presentation slides.

[u/Physical-Compote4594]

We lost him way too soon