Computer-assisted proofs and their understanding by a human: the case of univalent foundations

The computer-assisted proof of Four Colour Map theorem published by Kenneth Appel, Wolfgang Haken and John Koch back in 1977 prompted a continued philosophical discussion on the epistemic value of computer-assisted mathematical proofs. We show, developing the approach proposed by O.B. Brassler in 2006, how the Univalent Foundations of Mathematics (UF) meets some earlier stressed epistemological concerns about computer-assisted proofs and thus offers a new possibility to fill the gap between computer-assisted and traditional mathematical proofs. We demonstrate the argument with a simple computer-assisted proof from Algebraic Topology.