Re:New math book rescues landmark topology proof
by qsort on Thursday September 09, 2021 @02:33PM
(#28473009)
For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve.
Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.
Re:New math book rescues landmark topology proof
by lostmsu on Thursday September 09, 2021 @02:52PM
(#28473206)
There are multiple ways in which Google Mail while behaving incorrectly still be usable. But a theorem is not only useless if it is incorrect, it is dangerous.
Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.