> With something like Lean, you don’t need a human verifier.
The purpose of a proof is to show yourself and someone else why something is true. I don’t know what it would mean to be writing them for computers to verify. Unless the only thing you are interested in is y/n
Humans make mistakes. The more complex our mathematics become, the higher the chance that mistakes creep in. If you want mathematical foundations to be solid you need to minimize the number of wrong theorems we build on.
The purpose of a proof is to show yourself and someone else why something is true. I don’t know what it would mean to be writing them for computers to verify. Unless the only thing you are interested in is y/n