I'm not sure if it's really the foundations that are the biggest barrier to entry for mathematicians (at least for most fields of math). Admittedly, I don't have experience with dependent-type based systems such as Coq/Agda, which, incidentally, are what the authors use to formalize their Univalent Foundations. But at least for HOL-based systems (e.g. Isabelle/HOL or HOL4), you don't really need to understand their foundations in order to work with them. Oddly enough, they're neither the standard (first-order, that is, predicate logic based) ZFC theory, nor the Univalent foundations.
Isabelle in particular already has reasonably large formalizations of classic results in analysis and linear algebra. It also has a nice structured input language which makes the proofs relatively similar to the standard mathematical language. Here's a formalization of the Hahn-Banach theorem (a central result of functional analysis):
(the rendering is not complete, as many special symbols aren't replaced in the HTML version - it looks nicer when opened in Isabelle itself). If you're interested in learning more, you can start with the "new" tutorial:
Anyway, I think that computer proofs are going to remain harder for the foreseeable future, no matter what the foundations. Human written proofs tend to skip and conflate many small steps, and this is exactly what makes them easier and faster to write. Ideally, the verification system would perform this small steps automatically on your behalf. They're getting better at that (the sledgehammer tool in Isabelle is great), but still very far away from what you'd need.
Until that happens I don't expect to see pervasive machine-assisted proofs anywhere. Not least because of the dynamics of modern academia. It's publish or perish, and if doing computer proofs slows you down, a lot of people are going to chose not to do them, and this sets a standard in the field (where such proofs are not particularly valued).
The whole post of course comes with a big caveat: I'm not familiar with Univalent Foundations (I watched the video but that doesn't really discuss them). If I'm wrong in my views I would love some UF experts to chime in.
Isabelle in particular already has reasonably large formalizations of classic results in analysis and linear algebra. It also has a nice structured input language which makes the proofs relatively similar to the standard mathematical language. Here's a formalization of the Hahn-Banach theorem (a central result of functional analysis):
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/H...
(the rendering is not complete, as many special symbols aren't replaced in the HTML version - it looks nicer when opened in Isabelle itself). If you're interested in learning more, you can start with the "new" tutorial:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2...
Anyway, I think that computer proofs are going to remain harder for the foreseeable future, no matter what the foundations. Human written proofs tend to skip and conflate many small steps, and this is exactly what makes them easier and faster to write. Ideally, the verification system would perform this small steps automatically on your behalf. They're getting better at that (the sledgehammer tool in Isabelle is great), but still very far away from what you'd need.
Until that happens I don't expect to see pervasive machine-assisted proofs anywhere. Not least because of the dynamics of modern academia. It's publish or perish, and if doing computer proofs slows you down, a lot of people are going to chose not to do them, and this sets a standard in the field (where such proofs are not particularly valued).
The whole post of course comes with a big caveat: I'm not familiar with Univalent Foundations (I watched the video but that doesn't really discuss them). If I'm wrong in my views I would love some UF experts to chime in.