Thanks, I'd imagine an extremely small number of proofs could be verified this way

There are archives of formal proofs that are quite big, e.g. https://www.isa-afp.org/ for Isabelle, https://github.com/UniMath for Coq

Thanks! This is really fascinating for me, i had never heard of this way of doing proofs and I studied math in college