3 ms·
So would it be fair to say then, that these proof checkers are missing the 'libraries' that would be needed to efficiently write verifiable proofs for modern ma
by xyzzy123 14y ago
So would it be fair to say then, that these proof checkers are missing the 'libraries' that would be needed to efficiently write verifiable proofs for modern mathematics?
- cperciva 14y agoExactly. And this is where most of the work on proof checkers is happening -- finding ways that people can input proofs in a less formal way and have automated code fill in the formal details as a first pass before running the verification.
- makmanalp 14y agoIndeed! This is exactly what I was trying to say!