| ▲ | DoctorOetker 2 days ago | |
Sure the history of mathematics used many alternative conceptions of "proof". The problem is that such constructions were later found to be full of hidden assumptions. Like working in a plane vs on a spherical surface etc. The advantage of systems like MetaMath are: 1. prover and verifier are essentially separate code bases, indeed the MM prover is essentially absent, its up to humans or other pieces of software to generate proofs. The database just contains explicit axioms, definitions, theorems claims, with proofs for each theorem. The verifier is a minimalistic routine with a minimum amount of lines of code (basically substitution maps, with strict conditions). The proof is a concrete object, a finite list of steps. 2. None of the axioms are hardcoded or optimized, like they tend to be in proof systems where proof search and verification are intermixed, forcing axioms upon the user. | ||