Voevodsky developed Univalent Foundations in order to catch subtle mistakes in his (and others) result:
"Only then did I discover that the proof of a
key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.
This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident."
More details on page 8 in the IAS newsletter article
Look into the Coq language, it is under active development and there is a lot of work going into it. Voevodsky was working in Coq, if I recall.
As to how hard it is to learn, you will have to learn a pretty decent amount. It all depends on your background. If you know what the Curry Howard correspondence is, you are in relatively good shape. If you've never heard of lambda calculus or first order logic, you may have some more work cut out for you.
Here is a nice article I read last night on explaining the move from set theory to type theory. It gets a bit technical but you might be able to get something from it.
"Only then did I discover that the proof of a key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.
This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident."
More details on page 8 in the IAS newsletter article
https://www.ias.edu/sites/default/files/pdfs/publications/le...
There is also a Quanta article:
https://www.quantamagazine.org/univalent-foundations-redefin...