3 ms·

Ensuring the proof is actually one https://www.quantamagazine.org/in-computers-we-trust-20130222/ https://www.quantamagazine.org/in-computers-we-trust-2013022.

• imranq 7y ago
  Thanks, I'd imagine an extremely small number of proofs could be verified this way
  • brohee 7y ago
    There are archives of formal proofs that are quite big, e.g. https://www.isa-afp.org/ https://www.isa-afp.org/ for Isabelle, https://github.com/UniMath https://github.com/UniMath for Coq
    • imranq 7y ago
      Thanks! This is really fascinating for me, i had never heard of this way of doing proofs and I studied math in college