Metamath is a project to construct mathematics as proofs in ZFC. This what what we’re all supposed to be doing but in practice proofs tend to be informal arguments that we can convince people could be converted into derivations in ZFC. It looks like a long haul. There are now over 5000 theorems proved but they’ve only just proved a<=b => a<=b+1 in the reals. On the other hand they seem to have several hundred proofs about Hilbert spaces and quantum logic. Meanwhile, Wim Hesselink is hoping to verify a proof of Fermat’s Last Theorem by machine.