Absolutely correct. That said, proof assistants are being used. Here's a quote from TFA: > Lawrence Paulson, professor of computational logic and inventor of

Absolutely correct. That said, proof assistants are being used. Here's a quote from TFA: > Lawrence Paulson, professor of computational logic and inventor of Isabelle: > > [...] This identity holds in quite a few different proof assistants now.