Hacker News new | ask | show | jobs
by segfaultbuserr 1354 days ago
I remember seeing a post on MathOverflow, the OP asked about the consequences of using malicious code to fool a theorem prover to certify lies and falsehoods.

It's a valid question and has deep philosophical implications. Unfortunately, mathematicians are not tech workers, so they were not impressed, and closed the question as off-topic. I personally think the main reason resposible for the lack of enthusiasm from mathematicians is that formal methods are rarely used in our society, and mathematicians in general (with the exception of logicians) also do not really value formal axiomatic systems as the something especially important for setting a standard of truth. If formal methods are used in decision and policymaking in the far future, the picture will be different. Nevertheless, right now, malicious proofs are just a hypothetical thought experiment.

https://mathoverflow.net/questions/63816/consequences-of-tec...