Non-math person here. Wait, so you're saying it's easier for humans to prove complex theorems than computers? That's nuts.
Doesn't that mean that verifying proofs is then based on a super handwavy process where a bunch of researchers come to a consensus and say "yes, this is correct"? Ugh!
What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions?
When you describe a proof with words like you say, aren't there quibbles over semantic things? But I thought the whole point of a proof was that you leave nothing to semantics. Everything logically follows from each other.
I thought the main issue with proofs systems was that encoding the concepts into code was tedious. Could we maybe have a common database of well-known proofs, axioms, concepts etc, so that you wouldn't have to rewrite common ideas from scratch? Like a package manager with proof-libraries?
Or is this an issue with the expression power of proofs languages?
Doesn't that mean that verifying proofs is then based on a super handwavy process where a bunch of researchers come to a consensus and say "yes, this is correct"? Ugh!
What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions?
When you describe a proof with words like you say, aren't there quibbles over semantic things? But I thought the whole point of a proof was that you leave nothing to semantics. Everything logically follows from each other.
I thought the main issue with proofs systems was that encoding the concepts into code was tedious. Could we maybe have a common database of well-known proofs, axioms, concepts etc, so that you wouldn't have to rewrite common ideas from scratch? Like a package manager with proof-libraries?
Or is this an issue with the expression power of proofs languages?