Math is wrong... Mmmh I would have the tendency to disagree with this point 3. Haven't the proofs been deeply checked by peers when released? Following the reasoning of the point raised, this would mean we cannot trust our peers anymore. That's slightly overdoing it IMO.
You are viewing a single comment's thread from:
In the past, I've read objections to automated theorem provers from the opposite perspective. I kept waiting for that article to bring it up, but they never did. You never know if there's a bug in the code that might lead to a bad proof, so you can't consider something to be proved unless it has been through human peer review.
For things with large real world costs and consequences, I think it's a good idea to have both human and automated inspection, but that's more of an engineering thing than number theory. There's a cost involved in translating from mathematical notation to a language that the theorem prover understands, so you have to choose the places where you're going to go through all that effort.
Time (and thus money), as usual. However, you are right. As long as humans are still involved in the process, it is probably fine.