= 27d567bc2d48d9f40e9ccc20ea370b15)
MrMind comments on Open thread, Nov. 23 - Nov. 29, 2015 - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (257)
It always seemed very strange to me how, despite the obvious similarities and overlaps between mathematics and computer science, the use of computers for mathematics has largely been a fringe movement and mathematicians mostly still do mathematics the way it was done in the 19th century. This even though precision and accuracy is highly valued in mathematics and decades of experience in computer science has shown us just how prone humans are to making mistakes in programs, proofs, etc. and just how stubbornly these mistakes can evade the eyes of proof-checkers.
I think the difficulty is in part due to the fact that mathematicians use classical metalogic (e.g. proof by contradiction) which is not easily implemented in a computer system. The most famous mathematical assistant, Coq, is based on a constructive type theory. Even the univalence program, which is ambitious in its goal to formalize all mathematics, is based on a variant of intuitionistic meta-logic.